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:3;
A3:
M c= N
by A1, CARD_1:3;
now ( not L <> {} or K = 0 or exp (K,M) c= exp (L,N) )assume
L <> {}
;
( K = 0 or exp (K,M) c= exp (L,N) )then A4:
Funcs (
(N \ M),
L)
<> {}
;
0 c= card (Funcs ((N \ M),L))
;
then
0 in card (Funcs ((N \ M),L))
by A4, CARD_1:3;
then A5:
nextcard (Segm (card 0)) c= card (Funcs ((N \ M),L))
by CARD_1:def 3;
0 + 1
= 1
;
then A6:
Segm 1
c= card (Funcs ((N \ M),L))
by A5, Lm8, NAT_1:42;
A7:
M misses N \ M
by XBOOLE_1:79;
A8:
N = M \/ (N \ M)
by A3, XBOOLE_1:45;
Funcs (
M,
K)
c= Funcs (
M,
L)
by A2, FUNCT_5:56;
then A9:
exp (
K,
M)
c= card (Funcs (M,L))
by CARD_1:11;
A10:
exp (
L,
N)
= card [:(Funcs (M,L)),(Funcs ((N \ M),L)):]
by A7, A8, FUNCT_5:62;
A11:
card [:(Funcs (M,L)),(Funcs ((N \ M),L)):] = card [:(card (Funcs (M,L))),(card (Funcs ((N \ M),L))):]
by Th6;
(card (Funcs (M,L))) *` (card (Funcs ((N \ M),L))) = card [:(card (Funcs (M,L))),(card (Funcs ((N \ M),L))):]
;
then
1
*` (card (Funcs (M,L))) c= exp (
L,
N)
by A6, A10, A11, Th89;
then
card (Funcs (M,L)) c= exp (
L,
N)
by Th20;
hence
(
K = 0 or
exp (
K,
M)
c= exp (
L,
N) )
by A9;
verum end;
hence
( K = 0 or exp (K,M) c= exp (L,N) )
by A1; verum