consider X being set such that
A5: 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 A5; :: 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 A6: ( x = g & dom g = dom f & ( 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
A7: ( z in dom g & y = g . z ) by FUNCT_1:def 5;
( y in f . z & f . z = f . z & f . z in rng f ) by A6, A7, FUNCT_1:def 5;
hence y in union (rng f) by TARSKI:def 4; :: thesis: verum

end;

then x in Funcs (dom f),(union (rng f)) by A6, FUNCT_2:def 2;
hence x in X by A5, A6; :: thesis: verum