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;
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; verum