defpred S₁[ set , set ] means for f being Element of REAL * st $1 = f holds
$2 = Relax (f,n);
set X = REAL * ;

A1: now

let xx be set ; :: thesis: ( xx in REAL * implies ex y1 being set st S₁[xx,y1] )
assume xx in REAL * ; :: thesis: ex y1 being set st S₁[xx,y1]
then reconsider h = xx as Element of REAL * ;
thus ex y1 being set st S₁[xx,y1] :: thesis: verum

proof

take y1 = Relax (h,n); :: thesis: S₁[xx,y1]
thus S₁[xx,y1] ; :: thesis: verum

end;

end;

consider F being Function such that
A2: ( dom F = REAL * & ( for x being set st x in REAL * holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A1);

now

let y1 be set ; :: thesis: ( y1 in rng F implies y1 in REAL * )
assume y1 in rng F ; :: thesis: y1 in REAL *
then consider xx being set such that
A3: xx in dom F and
A4: y1 = F . xx by FUNCT_1:def 3;
reconsider h = xx as Element of REAL * by A2, A3;
y1 = Relax (h,n) by A2, A4;
hence y1 in REAL * ; :: thesis: verum

end;

then rng F c= REAL * by TARSKI:def 3;
then reconsider F = F as Element of Funcs ((REAL *),(REAL *)) by A2, FUNCT_2:def 2;
take F ; :: thesis: ( dom F = REAL * & ( for f being Element of REAL * holds F . f = Relax (f,n) ) )
thus dom F = REAL * by A2; :: thesis: for f being Element of REAL * holds F . f = Relax (f,n)
let f be Element of REAL * ; :: thesis: F . f = Relax (f,n)
thus F . f = Relax (f,n) by A2; :: thesis: verum