defpred S₁[ object ] means ex g being Function st
( $1 = product g & g in product X );
consider Y being set such that
A1: for x being object holds
( x in Y iff ( x in bool (Funcs ((dom X),(union (Union X)))) & S₁[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 X ) )

now :: thesis: ( ( for x being object st x in Y holds
ex g being Function st
( x = product g & g in product X ) ) & ( for x being object st ex g being Function st
( x = product g & g in product X ) & ex g being Function st
( x = product g & g in product 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 X ) by A1; :: thesis: for x being object st ex g being Function st
( x = product g & g in product X ) & ex g being Function st
( x = product g & g in product X ) holds
x in Y
let x be object ; :: thesis: ( ex g being Function st
( x = product g & g in product X ) & ex g being Function st
( x = product g & g in product X ) implies x in Y )
assume A2: ex g being Function st
( x = product g & g in product X ) ; :: thesis: ( ex g being Function st
( x = product g & g in product X ) implies x in Y )
given g being Function such that A3: x = product g and
A4: g in product X ; :: thesis: x in Y
A5: dom g = dom X by A4, CARD_3:9;
rng g c= Union X

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng g or t in Union X )
assume t in rng g ; :: thesis: t in Union 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 X and
A10: for v being object st v in dom X holds
h . v in X . v by A4, CARD_3:def 5;
( t in X . u & X . u in rng X ) by A8, A9, A10, A6, A7, FUNCT_1:def 3;
hence t in Union X by TARSKI:def 4; :: thesis: verum

end;

then Union g c= union (Union X) by ZFMISC_1:77;
then Funcs ((dom g),(Union g)) c= Funcs ((dom X),(union (Union X))) by A5, FUNCT_5:56;
then A11: bool (Funcs ((dom g),(Union g))) c= bool (Funcs ((dom X),(union (Union 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 X ) ) ; :: thesis: verum