let i, n be Element of 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),(- 1)) . 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, Th20; :: 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, Th19; :: thesis: verum

end;

end;