---

Step * of Lemma extend-name-morph-iota

∀I,K:Cname List. ∀f:name-morph(I;K). ∀z,x:Cname.
  (iota(z) o f[z:=x]) = (f o iota(x)) ∈ name-morph(I;[x / K]) supposing (¬(x ∈ K)) ∧ (¬(z ∈ I))
BY
{ (Auto THEN BLemma `name-morphs-equal` THEN Auto) }

1
1. I : Cname List
2. K : Cname List
3. f : name-morph(I;K)
4. z : Cname
5. x : Cname
6. ¬(x ∈ K)
7. ¬(z ∈ I)
⊢ (iota(z) o f[z:=x]) = (f o iota(x)) ∈ (nameset(I) ⟶ extd-nameset([x / K]))

---

Latex:

---

Latex:
\mforall{}I,K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}z,x:Cname.
    (iota(z)  o  f[z:=x])  =  (f  o  iota(x))  supposing  (\mneg{}(x  \mmember{}  K))  \mwedge{}  (\mneg{}(z  \mmember{}  I))


By

---

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

---

Home Index