set X = REAL * ;
set mi = ((n * n) + (3 * n)) + 1;
let F1, F2 be Element of Funcs ((REAL *),(REAL *)); ( dom F1 = REAL * & ( for f being Element of REAL * holds F1 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) & dom F2 = REAL * & ( for f being Element of REAL * holds F2 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) implies F1 = F2 )
assume that
A5:
dom F1 = REAL *
and
A6:
for f being Element of REAL * holds F1 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1))
and
A7:
dom F2 = REAL *
and
A8:
for f being Element of REAL * holds F2 . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1))
; F1 = F2
hence
F1 = F2
by A5, A7, FUNCT_1:2; verum