let N, M 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 by CARD_1:def 2;
card N = N by CARD_1:def 2;
then A3: M *` N = card (M *^ N) by A2, Th25;
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