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