deffunc H₁( Real, Element of REAL n) -> Element of REAL n = $1 * $2;
deffunc H₂( Element of REAL n, Element of REAL n) -> Element of REAL n = $1 + $2;
consider f being BinOp of (REAL n) such that
A1: for x, y being Element of REAL n holds f . (x,y) = H₂(x,y) from BINOP_1:sch 4();
consider g being Function of [:REAL,(REAL n):],(REAL n) such that
A2: for r being Element of REAL
for x being Element of REAL n holds g . (r,x) = H₁(r,x) from BINOP_1:sch 4();
set RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #);
A3: for r being Real
for x being Element of REAL n holds g . (r,x) = H₁(r,x)

let r be Real; :: thesis:
let x be Element of REAL n; :: thesis:
reconsider r = r as Element of REAL by XREAL_0:def 1;
g . (r,x) = H₁(r,x) by A2;
hence g . (r,x) = H₁(r,x) ; :: thesis:

end;

let u, v, w be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider u1 = u, v1 = v, w1 = w as Element of REAL n ;
thus (u + v) + w = f . ((u1 + v1),w) by A1
.= (u1 + v1) + w1 by A1
.= u1 + (v1 + w1) by FINSEQOP:28
.= f . (u,(v1 + w1)) by A1
.= u + (v + w) by A1 ; :: thesis:

end;

let v, w be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider v1 = v, w1 = w as Element of REAL n ;
thus v + w = v1 + w1 by A1
.= w + v by A1 ; :: thesis:

end;

let v be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider v1 = v as Element of n -tuples_on REAL ;
thus v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = v1 + (n |-> (In (0,REAL))) by A1
.= v by RVSUM_1:16 ; :: thesis:

end;

let r be Real; :: thesis:
let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider v1 = v, w1 = w as Element of REAL n ;
reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL ;
A8: dist (v,w) = (Pitag_dist n) . (v,w) by METRIC_1:def 1
.= |.(v1 - w1).| by EUCLID:def 6 ;
A9: ( r * v = r * v1 & r * w = r * w1 ) by A3;
thus dist ((r * v),(r * w)) = (Pitag_dist n) . ((r * v),(r * w)) by METRIC_1:def 1
.= |.((r * v2) - (r * w2)).| by A9, EUCLID:def 6
.= |.((r * v2) + (((- 1) * r) * w2)).| by RVSUM_1:49
.= |.((r * v2) + (r * (- w2))).| by RVSUM_1:49
.= |.(r * (v1 - w1)).| by RVSUM_1:51
.= |.r.| * (dist (v,w)) by A8, EUCLID:11 ; :: thesis:

end;

let u, w, v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider u1 = u, w1 = w, v1 = v as Element of REAL n ;
reconsider u2 = u1, w2 = w1, v2 = v1 as Element of n -tuples_on REAL ;
A11: ( v + u = v1 + u1 & w + u = w1 + u1 ) by A1;
thus dist (v,w) = (Pitag_dist n) . (v,w) by METRIC_1:def 1
.= |.(v1 - w1).| by EUCLID:def 6
.= |.(((v2 + u2) - u2) - w2).| by RVSUM_1:42
.= |.((v2 + u2) - (u2 + w2)).| by RVSUM_1:39
.= (Pitag_dist n) . ((v1 + u1),(w1 + u1)) by EUCLID:def 6
.= dist ((v + u),(w + u)) by A11, METRIC_1:def 1 ; :: thesis:

end;

let v be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: according to ALGSTR_0:def 16 :: thesis:
reconsider v1 = v as Element of n -tuples_on REAL ;
reconsider w = - v1 as Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis:
thus v + w = v1 - v1 by A1
.= 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) by RVSUM_1:37 ; :: thesis:

end;

let a1 be Real; :: thesis:
let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider a = a1 as Real ;
reconsider v1 = v, w1 = w as Element of REAL n ;
reconsider v2 = v1, w2 = w1 as Element of n -tuples_on REAL ;
a * (v + w) = g . (a,(v1 + w1)) by A1
.= a * (v2 + w2) by A3
.= (a * v1) + (a * w1) by RVSUM_1:51
.= f . ((a * v1),(a * w1)) by A1
.= f . ((g . (a,v)),(a * w1)) by A3
.= (a * v) + (a * w) by A3 ;
hence a1 * (v + w) = (a1 * v) + (a1 * w) ; :: thesis:

end;

let a1, b1 be Real; :: thesis:
let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider a = a1, b = b1 as Real ;
reconsider v1 = v as Element of REAL n ;
reconsider v2 = v1 as Element of n -tuples_on REAL ;
(a + b) * v = (a + b) * v2 by A3
.= (a * v1) + (b * v1) by RVSUM_1:50
.= f . ((a * v1),(b * v1)) by A1
.= f . ((g . (a,v)),(b * v1)) by A3
.= (a * v) + (b * v) by A3 ;
hence (a1 + b1) * v = (a1 * v) + (b1 * v) ; :: thesis:

end;

let a1, b1 be Real; :: thesis:
let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider a = a1, b = b1 as Real ;
reconsider v1 = v as Element of REAL n ;
reconsider v2 = v1 as Element of n -tuples_on REAL ;
(a * b) * v = (a * b) * v2 by A3
.= a * (b * v1) by RVSUM_1:49
.= g . (a,(b * v1)) by A3
.= a * (b * v) by A3 ;
hence (a1 * b1) * v = a1 * (b1 * v) ; :: thesis:

end;

let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider v1 = v as Element of n -tuples_on REAL ;
thus 1 * v = 1 * v1 by A3
.= v by RVSUM_1:52 ; :: thesis:

end;

let a, b, c be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis:
reconsider a1 = a, b1 = b, c1 = c as Element of REAL n ;
thus ( dist (a,b) = 0 implies a = b ) :: thesis:

end;

end;