deffunc H1( set ) -> set = ($1 `1) \/ ($1 `2);
defpred S1[ Function] means $1 .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } ;
defpred S2[ Function] means for s being Element of DISJOINT_PAIRS A st s in B holds
$1 . s in (s `1) \/ (s `2);
deffunc H2( Element of Funcs ((DISJOINT_PAIRS A),[A])) -> object = [ { ($1 . s1) where s1 is Element of DISJOINT_PAIRS A : ( $1 . s1 in s1 `2 & s1 in B ) } , { ($1 . s2) where s2 is Element of DISJOINT_PAIRS A : ( $1 . s2 in s2 `1 & s2 in B ) } ];
set N = { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2) } ;
set N9 = { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : g .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } } ;
set M = (DISJOINT_PAIRS A) /\ { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2) } ;
A7:
for g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st S2[g] holds
S1[g]
A13:
{ H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : S2[g] } c= { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : S1[g] }
from FRAENKEL:sch 1(A7);
A14:
B is finite
;
{ H1(s) where s is Element of DISJOINT_PAIRS A : s in B } is finite
from FRAENKEL:sch 21(A14);
then A15:
union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } is finite
by A1, FINSET_1:7;
A16:
{ H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : g .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } } is finite
from FRAENKEL:sch 25(A14, A15, A2);
(DISJOINT_PAIRS A) /\ { H2(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2) } c= DISJOINT_PAIRS A
by XBOOLE_1:17;
hence
(DISJOINT_PAIRS A) /\ { [ { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in B ) } , { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in B ) } ] where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2) } is Element of Fin (DISJOINT_PAIRS A)
by A13, A16, FINSUB_1:def 5; verum