let I1, I2 be Function of X,REAL ; :: thesis: ( ( for x being Element of X holds I1 . x = inf ((dist f,x) .: A) ) & ( for x being Element of X holds I2 . x = inf ((dist f,x) .: A) ) implies I1 = I2 )
assume that
A2: for x being Element of X holds I1 . x = inf ((dist f,x) .: A) and
A3: for x being Element of X holds I2 . x = inf ((dist f,x) .: A) ; :: thesis: I1 = I2

now

let x be Element of X; :: thesis: I1 . x = I2 . x
I1 . x = inf ((dist f,x) .: A) by A2;
hence I1 . x = I2 . x by A3; :: thesis: verum

end;

hence I1 = I2 by FUNCT_2:113; :: thesis: verum