---

Step * of Lemma biject_functionality

∀[A1,B1,A2,B2:Type].  ∀f:A1 ⟶ B1. (Bij(A1;B1;f) ⇐⇒ Bij(A2;B2;f)) supposing (B1 ≡ B2 and A1 ≡ A2)
BY
{ (Unfold `ext-eq` 0 THEN Auto THEN Auto THEN Repeat (ParallelLast) THEN Try ((DoSubsume THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A1,B1,A2,B2:Type].    \mforall{}f:A1  {}\mrightarrow{}  B1.  (Bij(A1;B1;f)  \mLeftarrow{}{}\mRightarrow{}  Bij(A2;B2;f))  supposing  (B1  \mequiv{}  B2  and  A1  \mequiv{}  A2)


By

---

Latex:
(Unfold  `ext-eq`  0  THEN  Auto  THEN  Auto  THEN  Repeat  (ParallelLast)  THEN  Try  ((DoSubsume  THEN  Auto)))

---

Home Index