let i, n be Nat; :: thesis: for f being Element of REAL * st i in dom f & f . i = - 1 & i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = - 1
let f be Element of REAL * ; :: thesis: ( i in dom f & f . i = - 1 & i <> ((n * n) + (3 * n)) + 1 implies ((findmin n) . f) . i = - 1 )
set k = Argmin ((OuterVx (f,n)),f,n);
set mi = ((n * n) + (3 * n)) + 1;
assume that
A1: i in dom f and
A2: ( f . i = - 1 & i <> ((n * n) + (3 * n)) + 1 ) ; :: thesis: ((findmin n) . f) . i = - 1
A3: ((findmin n) . f) . i = ((f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- jj))) . i by Def11;