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

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

hence
I1 = I2
; :: thesis: verumlet 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;I1 . x = lower_bound ((dist (f,x)) .: A) by A2;

hence I1 . x = I2 . x by A3; :: thesis: verum