let n be Element of NAT ; :: thesis: for f being Element of REAL * holds Argmin (OuterVx f,n),f,n <= n
let f be Element of REAL * ; :: thesis: Argmin (OuterVx f,n),f,n <= n
set IN = OuterVx f,n;
set Ak = Argmin (OuterVx f,n),f,n;

per cases ( OuterVx f,n <> {} or OuterVx f,n = {} ) ;

suppose OuterVx f,n <> {} ; :: thesis: Argmin (OuterVx f,n),f,n <= n

hence Argmin (OuterVx f,n),f,n <= n by Th30; :: thesis: verum

end;

suppose OuterVx f,n = {} ; :: thesis: Argmin (OuterVx f,n),f,n <= n

hence Argmin (OuterVx f,n),f,n <= n by Def10; :: thesis: verum

end;

end;