let K, L, M, N be Cardinal; :: thesis: ( ( 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 ) ) ; :: thesis: ( K = 0 or exp K,M c= exp L,N )
then A2: ( K c= L & M c= N ) by CARD_1:13;

now

assume L <> {} ; :: thesis: ( K = 0 or exp K,M c= exp L,N )
then Funcs (N \ M),L <> {} by FUNCT_2:11;
then ( card (Funcs (N \ M),L) <> 0 & 0 c= card (Funcs (N \ M),L) ) ;
then ( 0 in card (Funcs (N \ M),L) & 0 = card 0 ) by CARD_1:13;
then ( nextcard (card 0 ) c= card (Funcs (N \ M),L) & 0 + 1 = 1 ) by CARD_1:def 6;
then A3: ( 1 c= card (Funcs (N \ M),L) & card (Funcs M,L) c= card (Funcs M,L) ) by Lm1, NAT_1:43;
A4: M misses N \ M by XBOOLE_1:79;
then ( exp K,M = card (Funcs M,K) & exp L,N = card (Funcs N,L) & N = M \/ (N \ M) & {} = M /\ (N \ M) & Funcs M,K c= Funcs M,L ) by A2, CARD_2:def 3, FUNCT_5:63, XBOOLE_0:def 7, XBOOLE_1:45;
then A5: ( exp K,M c= card (Funcs M,L) & exp L,N = card [:(Funcs M,L),(Funcs (N \ M),L):] & card [:(Funcs M,L),(Funcs (N \ M),L):] = card [:(card (Funcs M,L)),(card (Funcs (N \ M),L)):] & (card (Funcs M,L)) *` (card (Funcs (N \ M),L)) = card [:(card (Funcs M,L)),(card (Funcs (N \ M),L)):] ) by A4, CARD_1:27, CARD_2:14, CARD_2:def 2, FUNCT_5:69;
then 1 *` (card (Funcs M,L)) c= exp L,N by A3, Th68;
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 A5, XBOOLE_1:1; :: thesis: verum

end;

hence ( K = 0 or exp K,M c= exp L,N ) by A1; :: thesis: verum