defpred S₁[ set , set ] means for Y being set st $1 = Y holds
$2 = f " Y;
A1: for y being set st y in bool (rng f) holds
ex x being set st S₁[y,x]

proof

let y be set ; :: thesis: ( y in bool (rng f) implies ex x being set st S₁[y,x] )
assume y in bool (rng f) ; :: thesis: ex x being set st S₁[y,x]
take f " y ; :: thesis: S₁[y,f " y]
thus S₁[y,f " y] ; :: thesis: verum

end;

A2: for y, x1, x2 being set st y in bool (rng f) & S₁[y,x1] & S₁[y,x2] holds
x1 = x2

proof

let y, x1, x2 be set ; :: thesis: ( y in bool (rng f) & S₁[y,x1] & S₁[y,x2] implies x1 = x2 )
assume that
y in bool (rng f) and
A3: for Y being set st y = Y holds
x1 = f " Y and
A4: for Y being set st y = Y holds
x2 = f " Y ; :: thesis: x1 = x2
thus x1 = f " y by A3
.= x2 by A4 ; :: thesis: verum

end;

consider g being Function such that
A5: ( dom g = bool (rng f) & ( for y being set st y in bool (rng f) holds
S₁[y,g . y] ) ) from FUNCT_1:sch 2(A2, A1);
take g ; :: thesis: ( dom g = bool (rng f) & ( for Y being set st Y c= rng f holds
g . Y = f " Y ) )
thus ( dom g = bool (rng f) & ( for Y being set st Y c= rng f holds
g . Y = f " Y ) ) by A5; :: thesis: verum