let K, L, M, N be Cardinal; ( ( not ( K in L & M in N ) & not ( K c= L & M in N ) & not ( K in L & M c= N ) & not ( K c= L & M c= N ) ) or K = 0 or exp K,M c= exp L,N )
assume A1:
( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) )
; ( K = 0 or exp K,M c= exp L,N )
A2:
K c= L
by A1, CARD_1:13;
A3:
M c= N
by A1, CARD_1:13;
now assume
L <> {}
;
( K = 0 or exp K,M c= exp L,N )then A4:
Funcs (N \ M),
L <> {}
by FUNCT_2:11;
0 c= card (Funcs (N \ M),L)
;
then
0 in card (Funcs (N \ M),L)
by A4, CARD_1:13;
then A5:
nextcard (card 0 ) c= card (Funcs (N \ M),L)
by CARD_1:def 6;
0 + 1
= 1
;
then A6:
1
c= card (Funcs (N \ M),L)
by A5, Lm3, NAT_1:43;
A7:
M misses N \ M
by XBOOLE_1:79;
A8:
exp K,
M = card (Funcs M,K)
by CARD_2:def 3;
A9:
exp L,
N = card (Funcs N,L)
by CARD_2:def 3;
A10:
N = M \/ (N \ M)
by A3, XBOOLE_1:45;
Funcs M,
K c= Funcs M,
L
by A2, FUNCT_5:63;
then A11:
exp K,
M c= card (Funcs M,L)
by A8, CARD_1:27;
A12:
exp L,
N = card [:(Funcs M,L),(Funcs (N \ M),L):]
by A7, A9, A10, FUNCT_5:69;
A13:
card [:(Funcs M,L),(Funcs (N \ M),L):] = card [:(card (Funcs M,L)),(card (Funcs (N \ M),L)):]
by CARD_2:14;
(card (Funcs M,L)) *` (card (Funcs (N \ M),L)) = card [:(card (Funcs M,L)),(card (Funcs (N \ M),L)):]
by CARD_2:def 2;
then
1
*` (card (Funcs M,L)) c= exp L,
N
by A6, A12, A13, Th136;
then
card (Funcs M,L) c= exp L,
N
by CARD_2:33;
hence
(
K = 0 or
exp K,
M c= exp L,
N )
by A11, XBOOLE_1:1;
verum end;
hence
( K = 0 or exp K,M c= exp L,N )
by A1; verum