---

Step * of Lemma classfun-res-disjoint-union-comb-as-parallel-eclass1

∀[Info,A,B,S:Type]. ∀[es:EO+(Info)]. ∀[X1:EClass(A)]. ∀[X2:EClass(B)]. ∀[e:E]. ∀[f1:Id ⟶ A ⟶ S ⟶ S]. ∀[f2:Id
                                                                                                             ⟶ B
                                                                                                             ⟶ S
                                                                                                             ⟶ S].
∀[s:S].
  ((f1 + f2 loc(e) X1 (+) X2@e s) = ((f1 o X1) || (f2 o X2)@e s) ∈ S) supposing 
     (disjoint-classrel(es;A;X1;B;X2) and 
     single-valued-classrel(es;X1;A) and 
     single-valued-classrel(es;X2;B) and 
     ((↑e ∈b X1) ∨ (↑e ∈b X2)))
BY
{ ((UnivCD THENA Auto) THEN DProdsAndUnions) }

1
1. Info : Type
2. A : Type
3. B : Type
4. S : Type
5. es : EO+(Info)
6. X1 : EClass(A)
7. X2 : EClass(B)
8. e : E
9. f1 : Id ⟶ A ⟶ S ⟶ S
10. f2 : Id ⟶ B ⟶ S ⟶ S
11. s : S
12. ↑e ∈b X1
13. single-valued-classrel(es;X2;B)
14. single-valued-classrel(es;X1;A)
15. disjoint-classrel(es;A;X1;B;X2)
⊢ (f1 + f2 loc(e) X1 (+) X2@e s) = ((f1 o X1) || (f2 o X2)@e s) ∈ S

2
1. Info : Type
2. A : Type
3. B : Type
4. S : Type
5. es : EO+(Info)
6. X1 : EClass(A)
7. X2 : EClass(B)
8. e : E
9. f1 : Id ⟶ A ⟶ S ⟶ S
10. f2 : Id ⟶ B ⟶ S ⟶ S
11. s : S
12. ↑e ∈b X2
13. single-valued-classrel(es;X2;B)
14. single-valued-classrel(es;X1;A)
15. disjoint-classrel(es;A;X1;B;X2)
⊢ (f1 + f2 loc(e) X1 (+) X2@e s) = ((f1 o X1) || (f2 o X2)@e s) ∈ S

---

Latex:

---

Latex:
\mforall{}[Info,A,B,S:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X1:EClass(A)].  \mforall{}[X2:EClass(B)].  \mforall{}[e:E].  \mforall{}[f1:Id
                                                                                                                                                                        {}\mrightarrow{}  A
                                                                                                                                                                        {}\mrightarrow{}  S
                                                                                                                                                                        {}\mrightarrow{}  S].
\mforall{}[f2:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  S  {}\mrightarrow{}  S].  \mforall{}[s:S].
    ((f1  +  f2  loc(e)  X1  (+)  X2@e  s)  =  ((f1  o  X1)  ||  (f2  o  X2)@e  s))  supposing 
          (disjoint-classrel(es;A;X1;B;X2)  and 
          single-valued-classrel(es;X1;A)  and 
          single-valued-classrel(es;X2;B)  and 
          ((\muparrow{}e  \mmember{}\msubb{}  X1)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  X2)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  DProdsAndUnions)

---

Home Index