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 NAT = 0 ;
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 number , 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();
set W = RLSMetrStruct(# ZS,FF,O,F,G #);
A4: for a, b being real number
for x being VECTOR of holds (a + b) * x = (a * x) + (b * x)

let a, b be real number ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
let x be VECTOR of ; :: thesis:
set c = a + b;
reconsider X = x as Element of ZS ;
(a + b) * x = H₂(a + b,X) by A3;
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 holds x + y = y + x

let x, y be VECTOR of ; :: 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;

let x, y, z be VECTOR of ; :: 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;

let x be VECTOR of ; :: 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 ;
let x be VECTOR of ; :: 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;

A5: for a being real number
for x, y being VECTOR of holds a * (x + y) = (a * x) + (a * y)

let a be real number ; :: thesis:
reconsider a = a as Real by XREAL_0:def 1;
let x, y be VECTOR of ; :: 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 A3; :: thesis:

end;

A6: for a, b being real number
for x being VECTOR of holds (a * b) * x = a * (b * x)

let a, b be real number ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
let x be VECTOR of ; :: thesis:
set c = a * b;
reconsider X = x as Element of ZS ;
(a * b) * x = H₂(a * b,X) by A3;
hence (a * b) * x = a * (b * x) by A3; :: thesis:

end;

for x being VECTOR of holds 1 * x = x

reconsider A' = 1 as Element of REAL ;
let x be VECTOR of ; :: thesis:
reconsider X = x as Element of ZS ;
1 * x = H₂(A',X) by A3;
hence 1 * x = x by TARSKI:def 1; :: thesis:

end;

hence RLSMetrStruct(# ZS,FF,O,F,G #) is RealLinearSpace-like by A5, A4, A6, RLVECT_1:def 9; :: thesis:
A7: for a, b, c being Point of 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 ; :: thesis:
A8: dist a,a = FF . a,a by METRIC_1:def 1
.= 0 by A1 ;
hence dist a,a = 0 ; :: thesis:
A9: a = 0 by TARSKI:def 1;
hence ( dist a,b = 0 implies a = b ) by TARSKI:def 1; :: thesis:
A10: b = 0 by TARSKI:def 1;
hence dist a,b = dist b,a by A9; :: thesis:
thus dist a,c <= (dist a,b) + (dist b,c) by A9, A10, A8; :: thesis:

end;

let r be Element of REAL ; :: thesis:
let v, w be VECTOR of ; :: thesis:
reconsider v1 = v, w1 = w as Element of ZS ;
X: FF . v1,w1 = H₁(v1,w1) by A1;
thus dist (r * v),(r * w) = FF . (r * v),(r * w) by METRIC_1:def 1
.= (abs r) * 0 by A1
.= (abs r) * H₁(v1,w1) by A1
.= (abs r) * (FF . v1,w1) by X
.= (abs r) * (dist v,w) by METRIC_1:def 1 ; :: thesis:

end;

let u, w, v be VECTOR of ; :: 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;