deffunc H_{1}( set ) -> set = ($1 `1) \/ ($1 `2);

defpred S_{1}[ Function] means $1 .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } ;

defpred S_{2}[ Function] means for s being Element of DISJOINT_PAIRS A st s in B holds

$1 . s in (s `1) \/ (s `2);

deffunc H_{2}( 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 = { H_{2}(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_{2}(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_{2}(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) } ;

_{2}[g] holds

S_{1}[g]
_{2}(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : S_{2}[g] } c= { H_{2}(g) where g is Element of Funcs ((DISJOINT_PAIRS A),[A]) : S_{1}[g] }
from FRAENKEL:sch 1(A7);

A14: B is finite ;

{ H_{1}(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: { H_{2}(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_{2}(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

defpred S

defpred S

$1 . s in (s `1) \/ (s `2);

deffunc H

set N = { H

g . s in (s `1) \/ (s `2) } ;

set N9 = { H

set M = (DISJOINT_PAIRS A) /\ { H

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

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

A2: now :: thesis: for g, h being Element of Funcs ((DISJOINT_PAIRS A),[A]) st g | B = h | B holds

H_{2}(g) = H_{2}(h)

A7:
for g being Element of Funcs ((DISJOINT_PAIRS A),[A]) st SH

let g, h be Element of Funcs ((DISJOINT_PAIRS A),[A]); :: thesis: ( g | B = h | B implies H_{2}(g) = H_{2}(h) )

defpred S_{3}[ set ] means g . $1 in $1 `1 ;

defpred S_{4}[ set ] means g . $1 in $1 `2 ;

defpred S_{5}[ set ] means h . $1 in $1 `1 ;

defpred S_{6}[ set ] means h . $1 in $1 `2 ;

assume A3: g | B = h | B ; :: thesis: H_{2}(g) = H_{2}(h)

then A4: for s being Element of DISJOINT_PAIRS A st s in B holds

( S_{3}[s] iff S_{5}[s] )
by FRAENKEL:1;

A5: { (g . s2) where s2 is Element of DISJOINT_PAIRS A : ( S_{3}[s2] & s2 in B ) } = { (h . t2) where t2 is Element of DISJOINT_PAIRS A : ( S_{5}[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_{4}[s] iff S_{6}[s] )
by A3, FRAENKEL:1;

{ (g . s1) where s1 is Element of DISJOINT_PAIRS A : ( S_{4}[s1] & s1 in B ) } = { (h . t1) where t1 is Element of DISJOINT_PAIRS A : ( S_{6}[t1] & t1 in B ) }
from FRAENKEL:sch 9(A3, A6);

hence H_{2}(g) = H_{2}(h)
by A5; :: thesis: verum

end;defpred S

defpred S

defpred S

defpred S

assume A3: g | B = h | B ; :: thesis: H

then A4: for s being Element of DISJOINT_PAIRS A st s in B holds

( S

A5: { (g . s2) where s2 is Element of DISJOINT_PAIRS A : ( S

A6: for s being Element of DISJOINT_PAIRS A st s in B holds

( S

{ (g . s1) where s1 is Element of DISJOINT_PAIRS A : ( S

hence H

S

proof

A13:
{ H
let g be Element of Funcs ((DISJOINT_PAIRS A),[A]); :: thesis: ( S_{2}[g] implies S_{1}[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_{1}[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;assume A8: for s being Element of DISJOINT_PAIRS A st s in B holds

g . s in (s `1) \/ (s `2) ; :: thesis: S

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

A14: B is finite ;

{ H

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: { H

(DISJOINT_PAIRS A) /\ { H

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