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 Th72;
then card M = (card 2) *` (card M) by Th13
.= card ((succ 1) *^ M) by Th13
.= card ((1 *^ M) +^ M) by ORDINAL2:36
.= M +` M by ORDINAL2:39 ;
hence M +` M = M ; :: thesis: verum