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: B is finite ;
A19: C is finite ;
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)));

A20: now

let f, f' be Element of Funcs (DISJOINT_PAIRS A),[:(Fin A),(Fin A):]; :: thesis: ( f | B = f' | B implies H₁(f) = H₁(f') )
assume f | B = f' | B ; :: thesis: H₁(f) = H₁(f')
then ((pair_diff A) .: f,(incl (DISJOINT_PAIRS A))) | B = ((pair_diff A) .: f',(incl (DISJOINT_PAIRS A))) | B by FUNCOP_1:29;
hence H₁(f) = H₁(f') by NORMFORM:41; :: thesis: verum

end;

{ 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(A18, A19, A20);
then (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 finite ;
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