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₂( 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();
deffunc H₃( real number , Element of ZS) -> Element of ZS = O;
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 x, y being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + y = y + x

proof

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) & y + x = H₂(Y,X) ) by A2;
hence x + y = y + x ; :: thesis:

end;

A5: for x, y, z being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (x + y) + z = x + (y + z)

proof

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) & x + (y + z) = H₂(X,H₂(Y,Z)) ) by A2;
hence (x + y) + z = x + (y + z) ; :: thesis:

end;

A6: for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds x + (0. RLSMetrStruct(# ZS,FF,O,F,G #)) = x

proof

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;

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

proof

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

end;

A8: for a, b being real number
for x being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds (a + b) * x = (a * x) + (b * x)

proof

let a, b be real number ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
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 A3;
hence (a + b) * x = (a * x) + (b * x) by A2; :: thesis:

end;

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

proof

let a, b be real number ; :: thesis:
reconsider a = a, b = b as Real by XREAL_0:def 1;
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 A3;
hence (a * b) * x = a * (b * x) by A3; :: thesis:

end;

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

proof

let x be VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
reconsider X = x as Element of ZS ;
reconsider A' = 1 as Element of REAL ;
1 * x = H₃(A',X) by A3;
hence 1 * x = x by TARSKI:def 1; :: thesis:

end;

A11: 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) )

proof

let a, b, c be Point of RLSMetrStruct(# ZS,FF,O,F,G #); :: thesis:
A12: ( a = 0 & b = 0 & c = 0 ) by TARSKI:def 1;
thus A13: dist a,a = 0 :: thesis:

proof

thus dist a,a = FF . a,a by METRIC_1:def 1
.= 0 by A1 ; :: thesis:

end;

thus ( dist a,b = 0 implies a = b ) by A12; :: thesis:
thus dist a,b = dist b,a by A12; :: thesis:
thus dist a,c <= (dist a,b) + (dist b,c) by A12, A13; :: thesis:

end;

A14: for r being Element of REAL
for v, w being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist (r * v),(r * w) = (abs r) * (dist v,w)

proof

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

end;

A15: for u, w, v being VECTOR of RLSMetrStruct(# ZS,FF,O,F,G #) holds dist v,w = dist (v + u),(w + u)

proof

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;

take RLSMetrStruct(# ZS,FF,O,F,G #) ; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is strict ; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is Abelian by A4, RLVECT_1:def 5; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is add-associative by A5, RLVECT_1:def 6; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is right_zeroed by A6, RLVECT_1:def 7; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is right_complementable :: thesis:

proof

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

end;

thus RLSMetrStruct(# ZS,FF,O,F,G #) is RealLinearSpace-like by A7, A8, A9, A10, RLVECT_1:def 9; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is Reflexive by A11, METRIC_1:1; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is discerning by A11, METRIC_1:2; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is symmetric by A11, METRIC_1:3; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is triangle by A11, METRIC_1:4; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is homogeneous by A14, Def5; :: thesis:
thus RLSMetrStruct(# ZS,FF,O,F,G #) is translatible by A15, Def6; :: thesis: