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, Th74;
N c= M
by A2, CARD_1:3;
then A4:
M +^ N c= M +^ M
by ORDINAL2:33;
A5:
M c= M +^ N
by ORDINAL3:24;
A6:
card M = M
;
A7:
M +` N c= M
by A3, A4, CARD_1:11;
M c= M +` N
by A5, A6, CARD_1:11;
hence
( M +` N = M & N +` M = M )
by A7; verum