let L, K, M, N be Cardinal; :: thesis: ( K in L & M in N implies ( K *` M in L *` N & M *` K in L *` N ) )
A1: for K, L, M, N being Cardinal st K in L & M in N & L c= N holds
K *` M in L *` N

proof

let K, L, M, N be Cardinal; :: thesis: ( K in L & M in N & L c= N implies K *` M in L *` N )
assume that
A2: K in L and
A3: M in N and
A4: L c= N ; :: thesis: K *` M in L *` N

A5: now :: thesis: ( N is finite implies K *` M in L *` N )

assume A6: N is finite ; :: thesis: K *` M in L *` N
then reconsider N = N as finite Cardinal ;
reconsider L = L, M = M, K = K as finite Cardinal by A2, A3, A4, A6, CARD_3:92;
A7: card (Segm N) = N ;
card (Segm M) = M ;
then card M < card N by A3, A7, NAT_1:41;
then A8: (card K) * (card M) <= (card K) * (card N) by XREAL_1:64;
A9: card (Segm L) = L ;
A10: L *` N = card (Segm ((card L) * (card N))) by CARD_2:39;
card (Segm K) = K ;
then card K < card L by A2, A9, NAT_1:41;
then (card K) * (card N) < (card L) * (card N) by A3, XREAL_1:68;
then A11: (card K) * (card M) < (card L) * (card N) by A8, XXREAL_0:2;
K *` M = card (Segm ((card K) * (card M))) by CARD_2:39;
hence K *` M in L *` N by A10, A11, NAT_1:41; :: thesis: verum

end;

A12: 0 in L by A2, ORDINAL3:8;

now :: thesis: ( not N is finite implies K *` M in L *` N )

assume A13: not N is finite ; :: thesis: K *` M in L *` N
then A14: L *` N = N by A4, A12, Th16;
A15: omega c= N by A13, CARD_3:85;

A16: now :: thesis: ( K is finite & M is finite implies K *` M in L *` N )

assume ( K is finite & M is finite ) ; :: thesis: K *` M in L *` N
then reconsider K = K, M = M as finite Cardinal ;
K *` M = card ((card K) * (card M)) by CARD_2:39
.= (card K) * (card M) ;
hence K *` M in L *` N by A14, A15; :: thesis: verum

end;

( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) ) ;
then ( ( K is finite & M is finite ) or K *` M c= M or ( K *` M c= K & K in N ) ) by A2, A4, Th17;
hence K *` M in L *` N by A3, A14, A16, ORDINAL1:12; :: thesis: verum

end;

hence K *` M in L *` N by A5; :: thesis: verum

end;

( L c= N or N c= L ) ;
hence ( K in L & M in N implies ( K *` M in L *` N & M *` K in L *` N ) ) by A1; :: thesis: verum