let M be Cardinal; :: thesis: ( not M is finite implies M +` M = M )
assume not M is finite ; :: thesis: M +` M = M
then M *^ 2 = M by Th30;
then card M = (card 2) *` (card M) by CARD_2:25
.= card ((succ 1) *^ M) by CARD_2:25
.= card ((1 *^ M) +^ M) by ORDINAL2:53
.= card (M +^ M) by ORDINAL2:56
.= M +` M by CARD_2:def 1 ;
hence M +` M = M by CARD_1:def 5; :: thesis: verum