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

proof

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

end;

A2: for x, y1, y2 being set st x in bool (dom f) & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: thesis: ( x in bool (dom f) & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
x in bool (dom f) and
A3: for X being set st x = X holds
y1 = f .: X and
A4: for X being set st x = X holds
y2 = f .: X ; :: thesis: y1 = y2
thus y1 = f .: x by A3
.= y2 by A4 ; :: thesis: verum

end;

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