let i, n be 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)),(- jj))) . i & Argmin ((OuterVx (f,n)),f,n) <= n ) by Def11, Th30;
hence ((findmin n) . f) . i = f . i by A1, Th18; :: thesis: verum