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