let n be 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);
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 Th29; :: 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;