deffunc H1( Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):])) -> Element of [:(Fin A),(Fin A):] = FinPairUnion (B,((pair_diff A) .: ($1,(incl (DISJOINT_PAIRS A)))));
set N = { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ;
set IT = (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } ;
A17: (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } c= DISJOINT_PAIRS A by XBOOLE_1:17;
A18: now :: thesis: for f, f9 being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) st f | B = f9 | B holds
H1(f) = H1(f9)
let f, f9 be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); :: thesis: ( f | B = f9 | B implies H1(f) = H1(f9) )
assume f | B = f9 | B ; :: thesis: H1(f) = H1(f9)
then ((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))) | B = ((pair_diff A) .: (f9,(incl (DISJOINT_PAIRS A)))) | B by FUNCOP_1:23;
hence H1(f) = H1(f9) by NORMFORM:22; :: thesis: verum
end;
A19: C is finite ;
A20: B is finite ;
{ H1(f) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } is finite from FRAENKEL:sch 25(A20, A19, A18);
 hence (DISJOINT_PAIRS A) /\ { (FinPairUnion (B,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: B c= C } is Element of Fin (DISJOINT_PAIRS A) by A17, FINSUB_1:def 5; :: thesis: verum