---

Step * of Lemma name-comp-flip

No Annotations
∀I:Cname List. ∀x:nameset(I). ∀K:Cname List. ∀f:name-morph(I;K). ∀f1:name-morph(K;[]).
  (f o flip(f1;f x)) = flip((f o f1);x) ∈ name-morph(I;[]) supposing ↑isname(f x)
BY
{ (Auto THEN (BLemma `name-morph-ext` THENA Auto) THEN FLemma `assert-isname` [-1] THEN Auto) }

1
1. I : Cname List
2. x : nameset(I)
3. K : Cname List
4. f : name-morph(I;K)
5. f1 : name-morph(K;[])
6. ↑isname(f x)
7. f x ∈ nameset(K)
8. x1 : nameset(I)
⊢ ((f o flip(f1;f x)) x1) = (flip((f o f1);x) x1) ∈ extd-nameset([])

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Cname  List.  \mforall{}x:nameset(I).  \mforall{}K:Cname  List.  \mforall{}f:name-morph(I;K).  \mforall{}f1:name-morph(K;[]).
    (f  o  flip(f1;f  x))  =  flip((f  o  f1);x)  supposing  \muparrow{}isname(f  x)


By

---

Latex:
(Auto  THEN  (BLemma  `name-morph-ext`  THENA  Auto)  THEN  FLemma  `assert-isname`  [-1]  THEN  Auto)

---

Home Index