---

Step * of Lemma sg-op_functionality

∀[sg:s-GroupStructure]. ∀[x1,y1,x2,y2:Point].  ((x1 y1) ≡ (x2 y2)) supposing (x1 ≡ x2 and y1 ≡ y2)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (FLemma `sg-op-sep` [-1] THENA Auto)
   THEN D -1
   THEN OnMaybeHyp 7 (\h. (D h THEN Trivial))) }

---

Latex:

---

Latex:
\mforall{}[sg:s-GroupStructure].  \mforall{}[x1,y1,x2,y2:Point].    ((x1  y1)  \mequiv{}  (x2  y2))  supposing  (x1  \mequiv{}  x2  and  y1  \mequiv{}  y2)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (FLemma  `sg-op-sep`  [-1]  THENA  Auto)
  THEN  D  -1
  THEN  OnMaybeHyp  7  (\mbackslash{}h.  (D  h  THEN  Trivial)))

---

Home Index