let K, L, 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

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 N = N by CARD_1:def 2;
A8: card M = M by CARD_1:def 2;
then card M < card N by A3, A7, NAT_1:41;
then A9: (card K) * (card M) <= (card K) * (card N) by XREAL_1:64;
A10: card L = L by CARD_1:def 2;
then A11: L *` N = card ((card L) * (card N)) by A7, CARD_2:39;
A12: card K = K by CARD_1:def 2;
then card K < card L by A2, A10, NAT_1:41;
then (card K) * (card N) < (card L) * (card N) by A3, XREAL_1:68;
then A13: (card K) * (card M) < (card L) * (card N) by A9, XXREAL_0:2;
K *` M = card ((card K) * (card M)) by A12, A8, CARD_2:39;
hence K *` M in L *` N by A11, A13, NAT_1:41; :: thesis: verum

end;

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

now

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

A18: now

assume ( K is finite & M is finite ) ; :: thesis: K *` M in L *` N
then reconsider K = K, M = M as finite Cardinal ;
( card K = K & card M = M ) by CARD_1:def 2;
then K *` M = card ((card K) * (card M)) by CARD_2:39
.= (card K) * (card M) by CARD_1:def 2 ;
hence K *` M in L *` N by A16, A17, TARSKI:def 3; :: 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, Th79;
hence K *` M in L *` N by A3, A16, A18, 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