---

Step * of Lemma module_eqfun_p

∀[A:Rng]. ∀[m:A-DModule]. ∀[x,y:m.car].  uiff(↑(x m.eq y);x = y ∈ m.car)
BY
{ ((Unfold `dmodule` 0 THEN Unfold `module` 0) THEN Auto THEN D 2 THEN Try ((Unhide THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:A-DModule].  \mforall{}[x,y:m.car].    uiff(\muparrow{}(x  m.eq  y);x  =  y)


By

---

Latex:
((Unfold  `dmodule`  0  THEN  Unfold  `module`  0)  THEN  Auto  THEN  D  2  THEN  Try  ((Unhide  THEN  Auto)))

---

Home Index