let n be Element of NAT ; :: thesis: for f being Element of REAL * st OuterVx (f,n) <> {} holds
ex j being Element of NAT st
( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )
let f be Element of REAL * ; :: thesis: ( OuterVx (f,n) <> {} implies ex j being Element of NAT st
( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 ) )
set IX = OuterVx (f,n);
assume OuterVx (f,n) <> {} ; :: thesis: ex j being Element of NAT st
( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )
then consider i being Element of NAT such that
A1: i = Argmin ((OuterVx (f,n)),f,n) and
A2: i in OuterVx (f,n) and
for k being Element of NAT st k in OuterVx (f,n) holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) and
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;
take i ; :: thesis: ( i in OuterVx (f,n) & 1 <= i & i <= n & ((findmin n) . f) . i = - 1 )
thus i in OuterVx (f,n) by A2; :: thesis: ( 1 <= i & i <= n & ((findmin n) . f) . i = - 1 )
A3: ex k being Element of NAT st
( i = k & k in dom f & 1 <= k & k <= n & f . k <> - 1 & f . (n + k) <> - 1 ) by A2;
hence ( 1 <= i & i <= n ) ; :: thesis: ((findmin n) . f) . i = - 1
thus ((findmin n) . f) . i = ((f,(((n * n) + (3 * n)) + 1)) := (i,(- 1))) . i by A1, Def11
.= - 1 by A3, Th20 ; :: thesis: verum