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 ((),[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 ((),[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 ((),[A]) : g .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } } ;
set M = () /\ { H2(g) where g is Element of Funcs ((),[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 ((),[A]) st g | B = h | B holds
H2(g) = H2(h)
let g, h be Element of Funcs ((),[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 A6: for s being Element of DISJOINT_PAIRS A st s in B holds
( S4[s] iff S6[s] ) by ;
{ (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 hence H2(g) = H2(h) by A5; :: thesis: verum
end;
A7: for g being Element of Funcs ((),[A]) st S2[g] holds
S1[g]
proof
let g be Element of Funcs ((),[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 ;
hence x in union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } by ; :: thesis: verum
end;
A13: { H2(g) where g is Element of Funcs ((),[A]) : S2[g] } c= { H2(g) where g is Element of Funcs ((),[A]) : S1[g] } from A14: B is finite ;
{ H1(s) where s is Element of DISJOINT_PAIRS A : s in B } is finite from then A15: union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } is finite by ;
A16: { H2(g) where g is Element of Funcs ((),[A]) : g .: B c= union { ((s `1) \/ (s `2)) where s is Element of DISJOINT_PAIRS A : s in B } } is finite from (DISJOINT_PAIRS A) /\ { H2(g) where g is Element of Funcs ((),[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 ((),[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 () by ; :: thesis: verum