---

Step * of Lemma zero_sym_grp

∀p:Sym(0). (p = id_perm() ∈ Sym(0))
BY
{ (D 0 THENA Auto) }

1
1. p : Sym(0)@i
⊢ p = id_perm() ∈ Sym(0)

---

Latex:

---

Latex:
\mforall{}p:Sym(0).  (p  =  id\_perm())


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index