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 assume
L <> {}
;
( K = 0 or exp (K,M) c= exp (L,N) )then A4:
Funcs (
(N \ M),
L)
<> {}
by FUNCT_2:8;
0 c= card (Funcs ((N \ M),L))
;
then
0 in card (Funcs ((N \ M),L))
by A4, CARD_1:3;
then A5:
nextcard (card 0) c= card (Funcs ((N \ M),L))
by CARD_1:def 3;
0 + 1
= 1
;
then A6:
1
c= card (Funcs ((N \ M),L))
by A5, Lm3, NAT_1:42;
A7:
M misses N \ M
by XBOOLE_1:79;
A8:
exp (
K,
M)
= card (Funcs (M,K))
;
A9:
exp (
L,
N)
= card (Funcs (N,L))
;
A10:
N = M \/ (N \ M)
by A3, XBOOLE_1:45;
Funcs (
M,
K)
c= Funcs (
M,
L)
by A2, FUNCT_5:56;
then A11:
exp (
K,
M)
c= card (Funcs (M,L))
by A8, CARD_1:11;
A12:
exp (
L,
N)
= card [:(Funcs (M,L)),(Funcs ((N \ M),L)):]
by A7, A9, A10, FUNCT_5:62;
A13:
card [:(Funcs (M,L)),(Funcs ((N \ M),L)):] = card [:(card (Funcs (M,L))),(card (Funcs ((N \ M),L))):]
by Th14;
(card (Funcs (M,L))) *` (card (Funcs ((N \ M),L))) = card [:(card (Funcs (M,L))),(card (Funcs ((N \ M),L))):]
by CARD_3: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 Th33;
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