Step * 2 of Lemma zhgrp_to_nat_is_hom


nat(e) 0 ∈ ℕ
BY
((RWH zhgrp_to_nat_downC THEN Auto) }


Latex:


Latex:

nat(e)  =  0


By


Latex:
((RWH  zhgrp\_to\_nat\_downC  0  )  THEN  Auto)




Home Index