deffunc H_{1}( Element of X) -> Element of REAL = In ((lower_bound ((dist (f,$1)) .: A)),REAL);

consider INF being Function of X,REAL such that

A1: for x being Element of X holds INF . x = H_{1}(x)
from FUNCT_2:sch 4();

take INF ; :: thesis: for x being Element of X holds INF . x = lower_bound ((dist (f,x)) .: A)

let x be Element of X; :: thesis: INF . x = lower_bound ((dist (f,x)) .: A)

INF . x = H_{1}(x)
by A1;

hence INF . x = lower_bound ((dist (f,x)) .: A) ; :: thesis: verum

consider INF being Function of X,REAL such that

A1: for x being Element of X holds INF . x = H

take INF ; :: thesis: for x being Element of X holds INF . x = lower_bound ((dist (f,x)) .: A)

let x be Element of X; :: thesis: INF . x = lower_bound ((dist (f,x)) .: A)

INF . x = H

hence INF . x = lower_bound ((dist (f,x)) .: A) ; :: thesis: verum