set X = REAL * ;

set mi = ((n * n) + (3 * n)) + 1;

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

$2 = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1));

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

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

rng F c= REAL *

take F ; :: thesis: ( dom F = REAL * & ( for f being Element of REAL * holds F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) )

thus dom F = REAL * by A2; :: thesis: for f being Element of REAL * holds F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1))

let f be Element of REAL * ; :: thesis: F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1))

thus F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) by A2; :: thesis: verum

set mi = ((n * n) + (3 * n)) + 1;

defpred S

$2 = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1));

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

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

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

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

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

then reconsider h = xx as Element of REAL * ;

reconsider y = (h,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (h,n)),h,n)),(- 1)) as object ;

take y = y; :: thesis: S_{1}[xx,y]

thus S_{1}[xx,y]
; :: thesis: verum

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

then reconsider h = xx as Element of REAL * ;

reconsider y = (h,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (h,n)),h,n)),(- 1)) as object ;

take y = y; :: thesis: S

thus S

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

S

rng F c= REAL *

proof

then reconsider F = F as Element of Funcs ((REAL *),(REAL *)) by A2, FUNCT_2:def 2;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in REAL * )

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

then consider xx being object such that

A3: xx in dom F and

A4: y = F . xx by FUNCT_1:def 3;

reconsider h = xx as Element of REAL * by A2, A3;

y = (h,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (h,n)),h,n)),(- 1)) by A2, A4;

hence y in REAL * by FINSEQ_1:def 11; :: thesis: verum

end;assume y in rng F ; :: thesis: y in REAL *

then consider xx being object such that

A3: xx in dom F and

A4: y = F . xx by FUNCT_1:def 3;

reconsider h = xx as Element of REAL * by A2, A3;

y = (h,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (h,n)),h,n)),(- 1)) by A2, A4;

hence y in REAL * by FINSEQ_1:def 11; :: thesis: verum

take F ; :: thesis: ( dom F = REAL * & ( for f being Element of REAL * holds F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) )

thus dom F = REAL * by A2; :: thesis: for f being Element of REAL * holds F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1))

let f be Element of REAL * ; :: thesis: F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1))

thus F . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) by A2; :: thesis: verum