:: deftheorem Def11 defines findmin GRAPHSP:def 11 :
for n being Nat
for b₂ being Element of Funcs ((REAL *),(REAL *)) holds
( b₂ = findmin n iff ( dom b₂ = REAL * & ( for f being Element of REAL * holds b₂ . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) ) );