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 N' = { 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 ) } ;
defpred S₁[ Function] means for s being Element of DISJOINT_PAIRS A st s in B holds
$1 . s in (s `1 ) \/ (s `2 );
defpred S₂[ Function] means $1 .: B c= union { ((s `1 ) \/ (s `2 )) where s is Element of DISJOINT_PAIRS A : s in B } ;
A1: 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 A2: 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
A3: y in dom g and
A4: y in B and
A5: x = g . y by FUNCT_1:def 12;
reconsider y = y as Element of DISJOINT_PAIRS A by A3;
A6: g . y in (y `1 ) \/ (y `2 ) by A2, A4;
(y `1 ) \/ (y `2 ) in { ((s `1 ) \/ (s `2 )) where s is Element of DISJOINT_PAIRS A : s in B } by A4;
hence x in union { ((s `1 ) \/ (s `2 )) where s is Element of DISJOINT_PAIRS A : s in B } by A5, A6, TARSKI:def 4; :: thesis: verum

end;

A7: { 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(A1);
A8: B is finite ;
deffunc H₂( set ) -> set = ($1 `1 ) \/ ($1 `2 );
A9: { H₂(s) where s is Element of DISJOINT_PAIRS A : s in B } is finite from FRAENKEL:sch 21(A8);

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;

then A10: union { ((s `1 ) \/ (s `2 )) where s is Element of DISJOINT_PAIRS A : s in B } is finite by A9, FINSET_1:25;

A11: 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 A12: g | B = h | B ; :: thesis: H₁(g) = H₁(h)
then A13: for s being Element of DISJOINT_PAIRS A st s in B holds
( S₄[s] iff S₆[s] ) by FRAENKEL:3;
A14: { (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(A12, A13);
A15: for s being Element of DISJOINT_PAIRS A st s in B holds
( S₃[s] iff S₅[s] ) by A12, FRAENKEL:3;
{ (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(A12, A15);
hence H₁(g) = H₁(h) by A14; :: thesis: verum

end;

A16: (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;
{ 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(A8, A10, A11);
then { 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 ) } is finite by A7;
then (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 ) } is finite ;
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 A16, FINSUB_1:def 5; :: thesis: verum