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

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