---

Step * of Lemma name-morph-inv-eq-domain

∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[x:name-morph-domain(f;I)].  ((name-morph-inv(I;f) (f x)) = x ∈ nameset(I))
BY
{ (InstLemma `name-morph-inv-eq` [] THEN RepeatFor 3 (ParallelLast') THEN (UnivCD THENA Auto)) }

1
1. I : Cname List
2. J : Cname List
3. f : name-morph(I;J)
4. ∀[x:nameset(I)]. (name-morph-inv(I;f) (f x)) = x ∈ nameset(I) supposing ↑isname(f x)
5. x : name-morph-domain(f;I)
⊢ (name-morph-inv(I;f) (f x)) = x ∈ nameset(I)

---

Latex:

---

Latex:
\mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[x:name-morph-domain(f;I)].
    ((name-morph-inv(I;f)  (f  x))  =  x)


By

---

Latex:
(InstLemma  `name-morph-inv-eq`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  (UnivCD  THENA  Auto))

---

Home Index