---

Step * of Lemma name-morph-extend-comp

∀[I,J,K:Cname List]. ∀[f:name-morph(I;J)]. ∀[g:name-morph(J;K)].  (((f o g))+ = ((f)+ o (g)+) ∈ name-morph(I+;K+))
BY
{ (Auto THEN BLemma `name-morphs-equal` THEN Auto) }

1
1. I : Cname List
2. J : Cname List
3. K : Cname List
4. f : name-morph(I;J)
5. g : name-morph(J;K)
⊢ ((f o g))+ = ((f)+ o (g)+) ∈ (nameset(I+) ⟶ extd-nameset(K+))

---

Latex:

---

Latex:
\mforall{}[I,J,K:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[g:name-morph(J;K)].    (((f  o  g))+  =  ((f)+  o  (g)+))


By

---

Latex:
(Auto  THEN  BLemma  `name-morphs-equal`  THEN  Auto)

---

Home Index