---

Step * of Lemma grp_op_wf

∀[g:GrpSig]. (* ∈ |g| ⟶ |g| ⟶ |g|)
BY
{ ModulePiTac 6 ``grp_car grp_eq grp_le grp_op grp_id grp_inv`` }

---

Latex:

---

Latex:
\mforall{}[g:GrpSig].  (*  \mmember{}  |g|  {}\mrightarrow{}  |g|  {}\mrightarrow{}  |g|)


By

---

Latex:
ModulePiTac  6  ``grp\_car  grp\_eq  grp\_le  grp\_op  grp\_id  grp\_inv``

---

Home Index