let n be Nat; :: thesis: for f being Element of REAL * st OuterVx (f,n) <> {} holds
ex j being 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 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 Nat st
( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )
then consider i being Nat such that
A1: i = Argmin ((OuterVx (f,n)),f,n) and
A2: i in OuterVx (f,n) and
for k being Nat st k in OuterVx (f,n) holds
f /. ((2 * n) + i) <= f /. ((2 * n) + k) and
for k being 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 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,(- jj))) . i by A1, Def11
.= - 1 by A3, Th19 ; :: thesis: verum