let M be Cardinal; :: thesis: for a being Aleph st ( a c= M or a in M ) holds
( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
let a be Aleph; :: thesis: ( ( a c= M or a in M ) implies ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) )
assume A1: ( a c= M or a in M ) ; :: thesis: ( a +` M = M & M +` a = M & a *` M = M & M *` a = M )
then ( not M is finite & card 0 in a & card 0 = 0 ) by Th25, Th26;
hence ( a +` M = M & M +` a = M & a *` M = M & M *` a = M ) by A1, CARD_3:118, CARD_4:78; :: thesis: verum