consider X being set such that
A11: for x being set 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 set holds
( x in X iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) )
let x be set ; :: thesis: ( x in X iff ex g being Function st
( x = g & dom g = dom f & ( for y being set 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 set st x in dom f holds
g . x in f . x ) ) ) by A11; :: thesis: ( ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) implies x in X )
given g being Function such that A12: x = g and
A13: dom g = dom f and
A14: for x being set 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 set ; :: 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 set such that
A15: z in dom g and
A16: y = g . z by FUNCT_1:def 3;
A17: y in f . z by A13, A14, A15, A16;
f . z in rng f by A13, A15, FUNCT_1:def 3;
hence y in union (rng f) by A17, TARSKI:def 4; :: thesis: verum

end;

then x in Funcs ((dom f),(union (rng f))) by A12, A13, FUNCT_2:def 2;
hence x in X by A11, A12, A13, A14; :: thesis: verum