set X = REAL * ;
set mi = ((n * n) + (3 * n)) + 1;
defpred S₁[ set , set ] 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));

A1: now

let xx be set ; :: thesis: ( xx in REAL * implies ex y being set st S₁[xx,y] )
assume xx in REAL * ; :: thesis: ex y being set st S₁[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 set ;
take y = y; :: thesis: S₁[xx,y]
thus S₁[xx,y] ; :: thesis: verum

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);
rng F c= REAL *

proof

let y be set ; :: 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 set such that
A3: xx in dom F and
A4: y = F . xx by FUNCT_1:def 5;
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;

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 = (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