deffunc H₁( set ) -> set = ($1 `1 ) \/ ($1 `2 );
defpred S₁[ Function] means $1 .: B c= union { ((s `1 ) \/ (s `2 )) where s is Element of DISJOINT_PAIRS A : s in B } ;
defpred S₂[ Function] means for s being Element of DISJOINT_PAIRS A st s in B holds
$1 . s in (s `1 ) \/ (s `2 );
deffunc H₂( Element of Funcs (DISJOINT_PAIRS A),[A]) -> set = [{ ($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 = { H₂(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 = { H₂(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) /\ { H₂(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

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

let g, h be Element of Funcs (DISJOINT_PAIRS A),[A]; :: thesis: ( g | B = h | B implies H₂(g) = H₂(h) )
defpred S₃[ set ] means g . $1 in $1 `1 ;
defpred S<sub>4</sub>[ set ] means g . $1 in $1 `2 ;
defpred S₅[ set ] means h . $1 in $1 `1 ;
defpred S<sub>6</sub>[ set ] means h . $1 in $1 `2 ;
assume A3: g | B = h | B ; :: thesis: H₂(g) = H₂(h)
then A4: for s being Element of DISJOINT_PAIRS A st s in B holds
( S₃[s] iff S₅[s] ) by FRAENKEL:3;
A5: { (g . s2) where s2 is Element of DISJOINT_PAIRS A : ( S₃[s2] & s2 in B ) } = { (h . t2) where t2 is Element of DISJOINT_PAIRS A : ( S₅[t2] & t2 in B ) } from FRAENKEL:sch 9(A3, A4);
A6: for s being Element of DISJOINT_PAIRS A st s in B holds
( S₄[s] iff S₆[s] ) by A3, FRAENKEL:3;
{ (g . s1) where s1 is Element of DISJOINT_PAIRS A : ( S₄[s1] & s1 in B ) } = { (h . t1) where t1 is Element of DISJOINT_PAIRS A : ( S₆[t1] & t1 in B ) } from FRAENKEL:sch 9(A3, A6);
hence H₂(g) = H₂(h) by A5; :: thesis: verum

end;

A7: for g being Element of Funcs (DISJOINT_PAIRS A),[A] st S₂[g] holds
S₁[g]

proof

let g be Element of Funcs (DISJOINT_PAIRS A),[A]; :: thesis: ( S₂[g] implies S₁[g] )
assume A8: for s being Element of DISJOINT_PAIRS A st s in B holds
g . s in (s `1 ) \/ (s `2 ) ; :: thesis: S₁[g]
let x be set ; :: 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 set such that
A9: y in dom g and
A10: y in B and
A11: x = g . y by FUNCT_1:def 12;
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: { H₂(g) where g is Element of Funcs (DISJOINT_PAIRS A),[A] : S₂[g] } c= { H₂(g) where g is Element of Funcs (DISJOINT_PAIRS A),[A] : S₁[g] } from FRAENKEL:sch 1(A7);
A14: B is finite ;
{ H₁(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:25;
A16: { H₂(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) /\ { H₂(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