deffunc H₁( set ) -> set = f . (x,$1);
A1: for y being set st y in X holds
H₁(y) in REAL

proof

let y be set ; :: thesis: ( y in X implies H₁(y) in REAL )
assume y in X ; :: thesis: H₁(y) in REAL
f . [x,y] in REAL ;
hence H₁(y) in REAL ; :: thesis: verum

end;

consider DIST being Function of X,REAL such that
A2: for y being set st y in X holds
DIST . y = H₁(y) from FUNCT_2:sch 2(A1);

now

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 4;
not y in dom DIST by A3;
hence f . (x,y) = DIST . y by A4, FUNCT_1:def 4; :: 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