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