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 A2: ( K in L & M in N & L c= N ) ; :: thesis: K *` M in L *` N
then A3: 0 in L by ORDINAL3:10;

A4: now

assume A5: 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, A5, CARD_3:111;
( card K = card (card K) & card K = K & card L = L & card M = M & card N = N ) by CARD_1:def 5;
then A6: ( K *` M = card ((card K) * (card M)) & L *` N = card ((card L) * (card N)) & card K < card L & card M < card N & 0 <= card K & 0 <= card M ) by A2, CARD_2:52, NAT_1:42;
then ( (card K) * (card M) <= (card K) * (card N) & (card K) * (card N) < (card L) * (card N) ) by XREAL_1:66, XREAL_1:70;
then (card K) * (card M) < (card L) * (card N) by XXREAL_0:2;
hence K *` M in L *` N by A6, NAT_1:42; :: thesis: verum

end;

now

assume not N is finite ; :: thesis: K *` M in L *` N
then A7: ( L *` N = N & omega c= N ) by A2, A3, Th78, CARD_3:102;
( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) ) ;
then A8: ( ( K is finite & M is finite ) or K *` M c= M or ( K *` M c= K & K in N ) ) by A2, Th79;

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 = card (card K) & card M = card (card M) & card K = K & card M = M ) by CARD_1:def 5;
then K *` M = card ((card K) * (card M)) by CARD_2:52
.= (card K) * (card M) by CARD_1:def 5 ;
hence K *` M in L *` N by A7, TARSKI:def 3; :: thesis: verum

end;

hence K *` M in L *` N by A2, A7, A8, ORDINAL1:22; :: thesis: verum

end;

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

end;

( K *` M = M *` K & L *` N = N *` L & ( 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