reconsider ZS = {0} as non empty set ;
reconsider O = 0 as Element of ZS by TARSKI:def 1;
deffunc H₁( Element of ZS, Element of ZS) -> Element of REAL = In (0,REAL);
consider FF being Function of [:ZS,ZS:],REAL such that
A1: for x, y being Element of ZS holds FF . (x,y) = H₁(x,y) from BINOP_1:sch 4();
deffunc H₂( Real, Element of ZS) -> Element of ZS = O;
deffunc H₃( Element of ZS, Element of ZS) -> Element of ZS = O;
consider F being BinOp of ZS such that
A2: for x, y being Element of ZS holds F . (x,y) = H₃(x,y) from BINOP_1:sch 4();
consider G being Function of [:REAL,ZS:],ZS such that
A3: for a being Element of REAL
for x being Element of ZS holds G . (a,x) = H₂(a,x) from BINOP_1:sch 4();
A4: for a being Real
for x being Element of ZS holds G . (a,x) = H₂(a,x)

let a be Real; :: thesis:
let x be Element of ZS; :: thesis:
reconsider a = a as Element of REAL by XREAL_0:def 1;
G . (a,x) = H₂(a,x) by A3;
hence G . (a,x) = H₂(a,x) ; :: thesis:

end;

set W = RLSMetrStruct(# ZS,FF,O,F,G #);
A5: for a, b being Real
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a + b) * x = (a * x) + (b * x)

let a, b be Real; :: thesis:
reconsider a = a, b = b as Real ;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
set c = a + b;
reconsider X = x as Element of ZS ;
(a + b) * x = H₂(a + b,X) by A4;
hence (a + b) * x = (a * x) + (b * x) by A2; :: thesis:

end;

take RLSMetrStruct(# ZS,FF,O,F,G #) ; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is strict ; :: thesis:
for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + y = y + x

let x, y be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider X = x, Y = y as Element of ZS ;
x + y = H₃(X,Y) by A2;
hence x + y = y + x by A2; :: thesis:

end;

hence RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian ; :: thesis:
for x, y, z being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (x + y) + z = x + (y + z)

let x, y, z be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider X = x, Y = y, Z = z as Element of ZS ;
(x + y) + z = H₃(H₃(X,Y),Z) by A2;
hence (x + y) + z = x + (y + z) by A2; :: thesis:

end;

hence RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative ; :: thesis:
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x

let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = H₃(X,O) by A2;
hence x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x by TARSKI:def 1; :: thesis:

end;

reconsider y = O as VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) ;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: according to ALGSTR_0:def 16 :: thesis:
take y ; :: according to ALGSTR_0:def 11 :: thesis:
thus x + y = 0. RLSMetrStruct(# ZS,FF,O,F,G #) by A2; :: thesis:

end;

A6: for a being Real
for x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds a * (x + y) = (a * x) + (a * y)

let a be Real; :: thesis:
reconsider a = a as Real ;
let x, y be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider X = x, Y = y as Element of ZS ;
(a * x) + (a * y) = H₃(H₂(a,X),H₂(a,Y)) by A2;
hence a * (x + y) = (a * x) + (a * y) by A4; :: thesis:

end;

A7: for a, b being Real
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a * b) * x = a * (b * x)

let a, b be Real; :: thesis:
reconsider a = a, b = b as Real ;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
set c = a * b;
reconsider X = x as Element of ZS ;
(a * b) * x = H₂(a * b,X) by A4;
hence (a * b) * x = a * (b * x) by A4; :: thesis:

end;

for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds 1 * x = x

reconsider A9 = 1 as Element of REAL by XREAL_0:def 1;
let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
1 * x = H₂(A9,X) by A4;
hence 1 * x = x by TARSKI:def 1; :: thesis:

end;

hence ( RLSMetrStruct(# ZS,FF,O,F,G #) is vector-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-distributive & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-associative & RLSMetrStruct(# ZS,FF,O,F,G #) is scalar-unital ) by A6, A5, A7; :: thesis:
A8: for a, b, c being Point of RLSMetrStruct(# ZS,FF,O,F,G #) holds
( dist (a,a) = 0 & ( dist (a,b) = 0 implies a = b ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )

let a, b, c be Point of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
A9: dist (a,a) = FF . (a,a) by METRIC_1:def 1
.= 0 by A1 ;
hence dist (a,a) = 0 ; :: thesis:
A10: a = 0 by TARSKI:def 1;
hence ( dist (a,b) = 0 implies a = b ) by TARSKI:def 1; :: thesis:
A11: b = 0 by TARSKI:def 1;
hence dist (a,b) = dist (b,a) by A10; :: thesis:
thus dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A10, A11, A9; :: thesis:

end;

let r be Real; :: thesis:
let v, w be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider v1 = v, w1 = w as Element of ZS ;
A12: FF . (v1,w1) = H₁(v1,w1) by A1;
thus dist ((r * v),(r * w)) = FF . ((r * v),(r * w)) by METRIC_1:def 1
.= |.r.| * 0 by A1
.= |.r.| * H₁(v1,w1)
.= |.r.| * (FF . (v1,w1)) by A12
.= |.r.| * (dist (v,w)) by METRIC_1:def 1 ; :: thesis:

end;

hence RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous ; :: thesis:
for u, w, v being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist (v,w) = dist ((v + u),(w + u))

let u, w, v be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
thus dist ((v + u),(w + u)) = FF . ((v + u),(w + u)) by METRIC_1:def 1
.= 0 by A1
.= FF . (v,w) by A1
.= dist (v,w) by METRIC_1:def 1 ; :: thesis:

end;