defpred S₂[ object ] means ex g being Function st
( $1 = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) );
consider A being set such that
A1: for x being object holds
( x in A iff ( x in PFuncs ((dom f),(union (rng f))) & S₂[x] ) ) from XBOOLE_0:sch 1();

now :: thesis:

let x be object ; :: thesis:
thus ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) by A1; :: thesis:
given g being Function such that A2: x = g and
A3: dom g c= dom f and
A4: for x being object st x in dom g holds
g . x in f . x ; :: thesis:
rng g c= union (rng f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
then consider z being object such that
A5: z in dom g and
A6: y = g . z by FUNCT_1:def 3;
A7: g . z in f . z by A4, A5;
f . z in rng f by A3, A5, FUNCT_1:def 3;
hence y in union (rng f) by A6, A7, TARSKI:def 4; :: thesis:

end;

then x in PFuncs ((dom f),(union (rng f))) by A2, A3, PARTFUN1:def 3;
hence x in A by A1, A2, A3, A4; :: thesis:

end;

hence ex b₁ being set st
for x being object holds
( x in b₁ iff ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) ; :: thesis: