for j, n being Nat
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 )