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

proof

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

end;

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

proof

let x, y1, y2 be object ; :: 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
reconsider x = x as set by TARSKI:1;
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 object 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