let M be Cardinal; :: thesis: ( not M is finite implies M +` M = M )
assume not M is finite ; :: thesis: M +` M = M
then M *^ (succ 1) = M by Th115;
then card M = (card 2) *` (card M) by Th25
.= card ((succ 1) *^ M) by Th25
.= card ((1 *^ M) +^ M) by ORDINAL2:36
.= card (M +^ M) by ORDINAL2:39
.= M +` M by CARD_3:def 1 ;
hence M +` M = M by CARD_1:def 2; :: thesis: verum