defpred S_{1}[ object , object ] means for f being Element of REAL * st $1 = f holds

$2 = Relax (f,n);

set X = REAL * ;

A2: ( dom F = REAL * & ( for x being object st x in REAL * holds

S_{1}[x,F . x] ) )
from CLASSES1:sch 1(A1);

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

$2 = Relax (f,n);

set X = REAL * ;

A1: now :: thesis: for xx being object st xx in REAL * holds

ex y1 being object st S_{1}[xx,y1]

consider F being Function such that ex y1 being object st S

let xx be object ; :: thesis: ( xx in REAL * implies ex y1 being object st S_{1}[xx,y1] )

assume xx in REAL * ; :: thesis: ex y1 being object st S_{1}[xx,y1]

then reconsider h = xx as Element of REAL * ;

thus ex y1 being object st S_{1}[xx,y1]
:: thesis: verum

end;assume xx in REAL * ; :: thesis: ex y1 being object st S

then reconsider h = xx as Element of REAL * ;

thus ex y1 being object st S

A2: ( dom F = REAL * & ( for x being object st x in REAL * holds

S

now :: thesis: for y1 being object st y1 in rng F holds

y1 in REAL *

then
rng F c= REAL *
;y1 in REAL *

let y1 be object ; :: thesis: ( y1 in rng F implies y1 in REAL * )

assume y1 in rng F ; :: thesis: y1 in REAL *

then consider xx being object 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;assume y1 in rng F ; :: thesis: y1 in REAL *

then consider xx being object 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

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