set X = REAL * ;
set mi = ((n * n) + (3 * n)) + 1;
let F1, F2 be Element of Funcs ((REAL *),(REAL *)); :: thesis: ( 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)) ; :: thesis: F1 = F2
now :: thesis: for xx being object st xx in dom F1 holds
F1 . xx = F2 . xx
let xx be object ; :: thesis: ( xx in dom F1 implies F1 . xx = F2 . xx )
assume xx in dom F1 ; :: thesis: F1 . xx = F2 . xx
then reconsider h = xx as Element of REAL * by A5;
thus F1 . xx = (h,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (h,n)),h,n)),(- 1)) by A6
.= F2 . xx by A8 ; :: thesis: verum
end;
hence F1 = F2 by A5, A7, FUNCT_1:2; :: thesis: verum