let M, N be Cardinal; ( not M is finite & ( N c= M or N in M ) implies ( M +` N = M & N +` M = M ) )
assume that
A1:
not M is finite
and
A2:
( N c= M or N in M )
; ( M +` N = M & N +` M = M )
A3:
M +` M = M
by A1, Th117;
A4:
M +` M = card (M +^ M)
by CARD_3:def 1;
A5:
M +` N = card (M +^ N)
by CARD_3:def 1;
N c= M
by A2, CARD_1:3;
then A6:
M +^ N c= M +^ M
by ORDINAL2:33;
A7:
M c= M +^ N
by ORDINAL3:24;
A8:
card M = M
by A3, A4;
A9:
M +` N c= M
by A3, A4, A5, A6, CARD_1:11;
M c= M +` N
by A5, A7, A8, CARD_1:11;
hence
( M +` N = M & N +` M = M )
by A9, XBOOLE_0:def 10; verum