---

Step * of Lemma product_functionality_wrt_equipollent

∀[A,B,C,D:Type].  (A ~ B ⇒ C ~ D ⇒ A × C ~ B × D)
BY
{ (Auto
   THEN (Assert A × C ~ B × C BY
               (BLemma `product_functionality_wrt_equipollent_left`  THEN Auto))
   THEN (Assert B × C ~ B × D BY
               (BLemma `product_functionality_wrt_equipollent_right`  THEN Auto))) }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. [D] : Type
5. A ~ B@i
6. C ~ D@i
7. A × C ~ B × C
8. B × C ~ B × D
⊢ A × C ~ B × D

---

Latex:

---

Latex:
\mforall{}[A,B,C,D:Type].    (A  \msim{}  B  {}\mRightarrow{}  C  \msim{}  D  {}\mRightarrow{}  A  \mtimes{}  C  \msim{}  B  \mtimes{}  D)


By

---

Latex:
(Auto
  THEN  (Assert  A  \mtimes{}  C  \msim{}  B  \mtimes{}  C  BY
                          (BLemma  `product\_functionality\_wrt\_equipollent\_left`    THEN  Auto))
  THEN  (Assert  B  \mtimes{}  C  \msim{}  B  \mtimes{}  D  BY
                          (BLemma  `product\_functionality\_wrt\_equipollent\_right`    THEN  Auto)))

---

Home Index