let M be Cardinal; :: thesis: M +` 0 = M
thus M +` 0 = card H₃(M, {} ) by Lm1
.= card M by CARD_1:69
.= M ; :: thesis: verum