defpred S1[ object ] means ex g being Function st
( $1 = product g & g in product ((Seg n) --> X) );
consider Y being set such that
A1: for x being object holds
( x in Y iff ( x in bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X))))) & S1[x] ) ) from XBOOLE_0:sch 1();
 take Y ; :: thesis: for f being object holds
( f in Y iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) )
now :: thesis: ( ( for x being object st x in Y holds
ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) ) & ( for x being object st ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) & ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) holds
x in Y ) )
thus for x being object st x in Y holds
ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) by A1; :: thesis: for x being object st ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) & ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) holds
x in Y
let x be object ; :: thesis: ( ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) & ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) implies x in Y )
assume A2: ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) ; :: thesis: ( ex g being Function st
( x = product g & g in product ((Seg n) --> X) ) implies x in Y )
given g being Function such that A3: x = product g and
A4: g in product ((Seg n) --> X) ; :: thesis: x in Y
A5: dom g = dom ((Seg n) --> X) by A4, CARD_3:9;
rng g c= Union ((Seg n) --> X)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in Union ((Seg n) --> X) )
assume t in rng g ; :: thesis: t in Union ((Seg n) --> X)
then consider u being object such that
A6: u in dom g and
A7: t = g . u by FUNCT_1:def 3;
consider h being Function such that
A8: g = h and
A9: dom h = dom ((Seg n) --> X) and
A10: for v being object st v in dom ((Seg n) --> X) holds
h . v in ((Seg n) --> X) . v by A4, CARD_3:def 5;
( t in ((Seg n) --> X) . u & ((Seg n) --> X) . u in rng ((Seg n) --> X) ) by A8, A9, A10, A6, A7, FUNCT_1:def 3;
hence t in Union ((Seg n) --> X) by TARSKI:def 4; :: thesis: verum
end;
then Union g c= union (Union ((Seg n) --> X)) by ZFMISC_1:77;
then Funcs ((dom g),(Union g)) c= Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X)))) by A5, FUNCT_5:56;
then A11: bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X))))) by ZFMISC_1:67;
product g c= Funcs ((dom g),(Union g)) by FUNCT_6:1;
hence x in Y by A2, A1, A3, A11; :: thesis: verum
end;
hence for f being object holds
( f in Y iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ; :: thesis: verum