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 5;
card N = N by CARD_1:def 5;
then A3: M *` N = card (M *^ N) by A2, CARD_2:25;
M c= M *^ N by A1, ORDINAL3:39;
hence ( M c= M *` N & M c= N *` M ) by A2, A3, CARD_1:27; :: thesis: verum