---

Step * of Lemma face-map-comp

∀A,B:Cname List. ∀g:name-morph(A;B). ∀x:nameset(A). ∀i:ℕ2.
  (g o (g x:=i)) = ((x:=i) o g) ∈ name-morph(A;B-[g x]) supposing ↑isname(g x)
BY
{ (Auto THEN FLemma `assert-isname` [-1] THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  FLemma  `assert-isname`  [-1]  THEN  Auto)

---

Home Index