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

now :: thesis: for x being Element of X holds I1 . x = I2 . x

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

end;

hence I1 = I2 ; :: thesis: verum