let i, n be Element of NAT ; :: thesis: for f being Element of REAL * st i > n & i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = f . i
let f be Element of REAL * ; :: thesis: ( i > n & i <> ((n * n) + (3 * n)) + 1 implies ((findmin n) . f) . i = f . i )
set k = Argmin (OuterVx f,n),f,n;
set mi = ((n * n) + (3 * n)) + 1;
assume A1: ( i > n & i <> ((n * n) + (3 * n)) + 1 ) ; :: thesis: ((findmin n) . f) . i = f . i
( ((findmin n) . f) . i = (f,(((n * n) + (3 * n)) + 1) := (Argmin (OuterVx f,n),f,n),(- 1)) . i & Argmin (OuterVx f,n),f,n <= n ) by Def11, Th31;
hence ((findmin n) . f) . i = f . i by A1, Th19; :: thesis: verum