let M, N be Cardinal; :: thesis: ( not M is finite & ( N c= M or N in M ) implies ( M +` N = M & N +` M = M ) )
assume ( not M is finite & ( N c= M or N in M ) ) ; :: thesis: ( M +` N = M & N +` M = M )
then A1: ( M +` M = M & M +` M = card (M +^ M) & M +` N = card (M +^ N) & N c= M & N = N & M = M ) by Th33, CARD_1:13, CARD_2:def 1;
then ( M +^ N c= M +^ M & M c= M +^ N & card M = M ) by ORDINAL2:50, ORDINAL3:27;
then ( M +` N c= M & M c= M +` N & M +` N = N +` M ) by A1, CARD_1:27;
hence ( M +` N = M & N +` M = M ) by XBOOLE_0:def 10; :: thesis: verum