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