deffunc H₁( object ) -> set = f . (x,$1);
A1: for y being object st y in X holds
H₁(y) in REAL by XREAL_0:def 1;
consider DIST being Function of X,REAL such that
A2: for y being object st y in X holds
DIST . y = H₁(y) from FUNCT_2:sch 2(A1);

now :: thesis: for y being Element of X holds f . (x,y) = DIST . y

per cases ( X is empty or not X is empty ) ;

suppose A3: X is empty ; :: thesis: for y being Element of X holds f . (x,y) = DIST . y

let y be Element of X; :: thesis: f . (x,y) = DIST . y
not [x,y] in dom f by A3;
then A4: f . [x,y] = {} by FUNCT_1:def 2;
not y in dom DIST by A3;
hence f . (x,y) = DIST . y by A4, FUNCT_1:def 2; :: thesis: verum

end;

suppose not X is empty ; :: thesis: for y being Element of X holds DIST . y = f . (x,y)

hence for y being Element of X holds DIST . y = f . (x,y) by A2; :: thesis: verum

end;

end;

end;

hence ex b₁ being Function of X,REAL st
for y being Element of X holds b₁ . y = f . (x,y) ; :: thesis: verum