---

Step * of Lemma face-map-comp-trivial

∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:Cname. ∀i:ℕ2.  ((x:=i) o g) = g ∈ name-morph(A;B) supposing ¬(x ∈ A)
BY
{ (Auto THEN Symmetry THEN BLemma `name-morph-ext` THEN Auto) }

1
1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : Cname
5. i : ℕ2
6. ¬(x ∈ A)
⊢ (x:=i) ∈ name-morph(A;A)

2
1. A : Cname List
2. B : Cname List
3. g : name-morph(A;B)
4. x : Cname
5. i : ℕ2
6. ¬(x ∈ A)
7. x1 : nameset(A)
⊢ (g x1) = (((x:=i) o g) x1) ∈ extd-nameset(B)

---

Latex:

---

Latex:
\mforall{}A,B:Cname  List.  \mforall{}g:name-morph(A;B).  \mforall{}x:Cname.  \mforall{}i:\mBbbN{}2.    ((x:=i)  o  g)  =  g  supposing  \mneg{}(x  \mmember{}  A)


By

---

Latex:
(Auto  THEN  Symmetry  THEN  BLemma  `name-morph-ext`  THEN  Auto)

---

Home Index