theorem Th31: :: GRAPHSP:31

for i, n being Nat
for f being Element of REAL * st i > n & i <> ((n * n) + (3 * n)) + 1 holds
((findmin n) . f) . i = f . i