let M, N be Cardinal; :: thesis: ( M c= M +` N & N c= M +` N )
A1: M c= M +^ N by ORDINAL3:24;
A2: N c= M +^ N by ORDINAL3:24;
A3: card N = N ;
card M = M ;
then A4: M c= card (M +^ N) by A1, CARD_1:11;
N c= card (M +^ N) by A2, A3, CARD_1:11;
hence ( M c= M +` N & N c= M +` N ) by A4; :: thesis: verum