let j, n be Nat; :: thesis: for f being Element of REAL * st OuterVx (f,n) <> {} & j = Argmin ((OuterVx (f,n)),f,n) holds
( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 )
let f be Element of REAL * ; :: thesis: ( OuterVx (f,n) <> {} & j = Argmin ((OuterVx (f,n)),f,n) implies ( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 ) )
set IN = OuterVx (f,n);
assume ( OuterVx (f,n) <> {} & j = Argmin ((OuterVx (f,n)),f,n) ) ; :: thesis: ( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 )
then ex i being Nat st
( i = j & i in OuterVx (f,n) & ( for k being Nat st k in OuterVx (f,n) holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in OuterVx (f,n) & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) by Def10;
then ex k being Nat st
( j = k & k in dom f & 1 <= k & k <= n & f . k <> - 1 & f . (n + k) <> - 1 ) ;
hence ( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 ) ; :: thesis: verum