let n, j be Element of 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 Element of NAT st
( i = j & i in OuterVx f,n & ( for k being Element of NAT st k in OuterVx f,n holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Element of NAT st k in OuterVx f,n & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds
i <= k ) ) by Def10;
then ex k being Element of 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