deffunc H₁( 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
H₁(f) = H₁(f9)

let f, f9 be Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]); :: thesis: ( f | B = f9 | B implies H₁(f) = H₁(f9) )
assume f | B = f9 | B ; :: thesis: H₁(f) = H₁(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 H₁(f) = H₁(f9) by NORMFORM:22; :: thesis: verum

end;

A19: C is finite ;
A20: B is finite ;
{ H₁(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