consider X being set such that
A14: for x being object holds
( x in X iff ( x in Funcs ((dom f),(union (rng f))) & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being object holds
( x in X iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) )
let x be object ; :: thesis: ( x in X iff ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) )
thus ( x in X implies ex g being Function st
( x = g & dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) ) by A14; :: thesis: ( ex g being Function st
( x = g & dom g = dom f & ( for y being object st y in dom f holds
g . y in f . y ) ) implies x in X )
given g being Function such that A15: x = g and
A16: dom g = dom f and
A17: for x being object st x in dom f holds
g . x in f . x ; :: thesis: x in X
rng g c= union (rng f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in union (rng f) )
assume y in rng g ; :: thesis: y in union (rng f)
then consider z being object such that
A18: z in dom g and
A19: y = g . z by FUNCT_1:def 3;
A20: y in f . z by A16, A17, A18, A19;
f . z in rng f by A16, A18, FUNCT_1:def 3;
hence y in union (rng f) by A20, TARSKI:def 4; :: thesis: verum

end;

then x in Funcs ((dom f),(union (rng f))) by A15, A16, FUNCT_2:def 2;
hence x in X by A14, A15, A16, A17; :: thesis: verum