deffunc H_{1}( object ) -> set = f . (x,$1);

A1: for y being object st y in X holds

H_{1}(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_{1}(y)
from FUNCT_2:sch 2(A1);

_{1} being Function of X,REAL st

for y being Element of X holds b_{1} . y = f . (x,y)
; :: thesis: verum

A1: for y being object st y in X holds

H

consider DIST being Function of X,REAL such that

A2: for y being object st y in X holds

DIST . y = H

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

hence
ex bper cases
( X is empty or not X is empty )
;

end;

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;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

for y being Element of X holds b