reconsider ZS = {0} as non empty set ;

deffunc H_{1}( Element of ZS, Element of ZS) -> Element of REAL = In (0,REAL);

consider F being Function of [:ZS,ZS:],REAL such that

A1: for x, y being Element of ZS holds F . (x,y) = H_{1}(x,y)
from BINOP_1:sch 4();

reconsider V = MetrStruct(# ZS,F #) as non empty MetrStruct ;

take V ; :: thesis: V is convex

let x, y be Element of V; :: according to VECTMETR:def 1 :: thesis: for r being Real st 0 <= r & r <= 1 holds

ex z being Element of V st

( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )

let r be Real; :: thesis: ( 0 <= r & r <= 1 implies ex z being Element of V st

( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) )

assume that

0 <= r and

r <= 1 ; :: thesis: ex z being Element of V st

( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )

take z = x; :: thesis: ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )

A6: dist (z,y) = F . (z,y) by METRIC_1:def 1

.= 0 by A1 ;

dist (x,z) = F . (x,z) by METRIC_1:def 1

.= 0 by A1 ;

hence ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) by A6; :: thesis: verum

deffunc H

consider F being Function of [:ZS,ZS:],REAL such that

A1: for x, y being Element of ZS holds F . (x,y) = H

reconsider V = MetrStruct(# ZS,F #) as non empty MetrStruct ;

A2: now :: thesis: for a, b being Element of V holds dist (a,b) = dist (b,a)

let a, b be Element of V; :: thesis: dist (a,b) = dist (b,a)

thus dist (a,b) = F . (a,b) by METRIC_1:def 1

.= 0 by A1

.= F . (b,a) by A1

.= dist (b,a) by METRIC_1:def 1 ; :: thesis: verum

end;thus dist (a,b) = F . (a,b) by METRIC_1:def 1

.= 0 by A1

.= F . (b,a) by A1

.= dist (b,a) by METRIC_1:def 1 ; :: thesis: verum

A3: now :: thesis: for a being Element of V holds dist (a,a) = 0

let a be Element of V; :: thesis: dist (a,a) = 0

thus dist (a,a) = F . (a,a) by METRIC_1:def 1

.= 0 by A1 ; :: thesis: verum

end;thus dist (a,a) = F . (a,a) by METRIC_1:def 1

.= 0 by A1 ; :: thesis: verum

A4: now :: thesis: for a, b, c being Element of V holds dist (a,c) <= (dist (a,b)) + (dist (b,c))

let a, b, c be Element of V; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))

A5: c = 0 by TARSKI:def 1;

a = 0 by TARSKI:def 1;

then ( b = 0 & dist (a,c) = 0 ) by A3, A5, TARSKI:def 1;

hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A5; :: thesis: verum

end;A5: c = 0 by TARSKI:def 1;

a = 0 by TARSKI:def 1;

then ( b = 0 & dist (a,c) = 0 ) by A3, A5, TARSKI:def 1;

hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A3, A5; :: thesis: verum

now :: thesis: for a, b being Element of V st dist (a,b) = 0 holds

a = b

then reconsider V = V as non empty Reflexive discerning symmetric triangle MetrStruct by A3, A2, A4, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4;a = b

let a, b be Element of V; :: thesis: ( dist (a,b) = 0 implies a = b )

assume dist (a,b) = 0 ; :: thesis: a = b

a = 0 by TARSKI:def 1;

hence a = b by TARSKI:def 1; :: thesis: verum

end;assume dist (a,b) = 0 ; :: thesis: a = b

a = 0 by TARSKI:def 1;

hence a = b by TARSKI:def 1; :: thesis: verum

take V ; :: thesis: V is convex

let x, y be Element of V; :: according to VECTMETR:def 1 :: thesis: for r being Real st 0 <= r & r <= 1 holds

ex z being Element of V st

( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )

let r be Real; :: thesis: ( 0 <= r & r <= 1 implies ex z being Element of V st

( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) )

assume that

0 <= r and

r <= 1 ; :: thesis: ex z being Element of V st

( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )

take z = x; :: thesis: ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) )

A6: dist (z,y) = F . (z,y) by METRIC_1:def 1

.= 0 by A1 ;

dist (x,z) = F . (x,z) by METRIC_1:def 1

.= 0 by A1 ;

hence ( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) by A6; :: thesis: verum