let M be Cardinal; :: thesis: M +` 0 = M
A1: ( [:{} ,{1}:] = {} & [:{} ,{0 }:] = {} ) by ZFMISC_1:113;
thus M +` 0 = card H₃(M, {} ) by Lm1
.= card M by A1, Th13
.= M by CARD_1:def 5 ; :: thesis: verum