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;

per cases ( i = Argmin ((OuterVx (f,n)),f,n) or i <> Argmin ((OuterVx (f,n)),f,n) ) ;

suppose i = Argmin ((OuterVx (f,n)),f,n) ; :: thesis: ((findmin n) . f) . i = - 1

hence ((findmin n) . f) . i = - 1 by A1, A3, Th19; :: thesis: verum

end;

suppose i <> Argmin ((OuterVx (f,n)),f,n) ; :: thesis: ((findmin n) . f) . i = - 1

hence ((findmin n) . f) . i = - 1 by A2, A3, Th18; :: thesis: verum

end;

end;