let M, N be Cardinal; :: thesis: ( N <> 0 implies ( M c= M *` N & M c= N *` M ) )
assume A1: N <> 0 ; :: thesis: ( M c= M *` N & M c= N *` M )
A2: card M = M ;
card N = N ;
then A3: M *` N = card (M *^ N) by A2, Th13;
M c= M *^ N by A1, ORDINAL3:36;
hence ( M c= M *` N & M c= N *` M ) by A2, A3, CARD_1:11; :: thesis: verum