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

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

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

( L c= N or N c= L )
;
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

end;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 )

A12:
0 in L
by A2, ORDINAL3:8;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;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

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

hence
K *` M in L *` N
by A5; :: thesis: verumassume 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;

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;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 )

( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) )
;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;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

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

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