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) } ;
A1: now :: thesis: for X being set st X in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } holds
X is finite
let X be set ; :: thesis: ( X in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } implies X is finite )
assume X in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } ; :: thesis: X is finite
then ex s being Element of DISJOINT_PAIRS A st
( X = (s `1) \/ (s `2) & s in B ) ;
hence X is finite ; :: thesis: verum
end;
A2: now :: thesis: for g, h being Element of Funcs ((DISJOINT_PAIRS A),[A]) st g | B = h | B holds
H2(g) = H2(h)
let g, h be Element of Funcs ((DISJOINT_PAIRS A),[A]); :: thesis: ( g | B = h | B implies H2(g) = H2(h) )
defpred S3[ set ] means g . $1 in $1 `1 ;
defpred S4[ set ] means g . $1 in $1 `2 ;
defpred S5[ set ] means h . $1 in $1 `1 ;
defpred S6[ set ] means h . $1 in $1 `2 ;
assume A3: g | B = h | B ; :: thesis: H2(g) = H2(h)
then A4: for s being Element of DISJOINT_PAIRS A st s in B holds
( S3[s] iff S5[s] ) by FRAENKEL:1;
A5: { (g . s2) where s2 is Element of DISJOINT_PAIRS A : ( S3[s2] & s2 in B ) } = { (h . t2) where t2 is Element of DISJOINT_PAIRS A : ( S5[t2] & t2 in B ) } from FRAENKEL:sch 9(A3, A4);
A6: for s being Element of DISJOINT_PAIRS A st s in B holds
( S4[s] iff S6[s] ) by A3, FRAENKEL:1;
{ (g . s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & s1 in B ) } = { (h . t1) where t1 is Element of DISJOINT_PAIRS A : ( S6[t1] & t1 in B ) } from FRAENKEL:sch 9(A3, A6);
hence H2(g) = H2(h) by A5; :: thesis: verum
end;
A7: for g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st S2[g] holds
S1[g]
proof
let g be Element of Funcs ((DISJOINT_PAIRS A),[A]); :: thesis: ( S2[g] implies S1[g] )
assume A8: for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1) \/ (s `2) ; :: thesis: S1[g]
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: B or x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } )
assume x in g .: B ; :: thesis: x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B }
then consider y being object such that
A9: y in dom g and
A10: y in B and
A11: x = g . y by FUNCT_1:def 6;
reconsider y = y as Element of DISJOINT_PAIRS A by A9;
A12: (y `1) \/ (y `2) in { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } by A10;
g . y in (y `1) \/ (y `2) by A8, A10;
hence x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } by A11, A12, TARSKI:def 4; :: thesis: verum
end;
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; :: thesis: verum