deffunc H1( Real, Element of REAL n) -> Element of REAL n = \$1 * \$2;
deffunc H2( 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) = H2(x,y) from 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) = H1(r,x) from set RLSMS = RLSMetrStruct(# (REAL n),(),(0* n),f,g #);
A3: for r being Real
for x being Element of REAL n holds g . (r,x) = H1(r,x)
proof
let r be Real; :: thesis: for x being Element of REAL n holds g . (r,x) = H1(r,x)
let x be Element of REAL n; :: thesis: g . (r,x) = H1(r,x)
reconsider r = r as Element of REAL by XREAL_0:def 1;
g . (r,x) = H1(r,x) by A2;
hence g . (r,x) = H1(r,x) ; :: thesis: verum
end;
A4: now :: thesis: for u, v, w being Element of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (u + v) + w = u + (v + w)
let u, v, w be Element of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: (u + v) + w = u + (v + w)
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: verum
end;
A5: now :: thesis: for v, w being Element of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds v + w = w + v
let v, w be Element of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: v + w = w + v
reconsider v1 = v, w1 = w as Element of REAL n ;
thus v + w = v1 + w1 by A1
.= w + v by A1 ; :: thesis: verum
end;
A6: now :: thesis: for v being Element of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds v + (0. RLSMetrStruct(# (REAL n),(),(0* n),f,g #)) = v
let v be Element of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: v + (0. RLSMetrStruct(# (REAL n),(),(0* n),f,g #)) = v
reconsider v1 = v as Element of n -tuples_on REAL ;
thus v + (0. RLSMetrStruct(# (REAL n),(),(0* n),f,g #)) = v1 + (n |-> (In (0,REAL))) by A1
.= v by RVSUM_1:16 ; :: thesis: verum
end;
A7: now :: thesis: for r being Real
for v, w being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))
let r be Real; :: thesis: for v, w being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))
let v, w be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: dist ((r * v),(r * w)) = |.r.| * (dist (v,w))
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) = () . (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)) = () . ((r * v),(r * w)) by METRIC_1:def 1
.= |.((r * v2) - (r * w2)).| by
.= |.((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 ; :: thesis: verum
end;
A10: now :: thesis: for u, w, v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds dist (v,w) = dist ((v + u),(w + u))
let u, w, v be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: dist (v,w) = dist ((v + u),(w + u))
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) = () . (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
.= () . ((v1 + u1),(w1 + u1)) by EUCLID:def 6
.= dist ((v + u),(w + u)) by ; :: thesis: verum
end;
A12: RLSMetrStruct(# (REAL n),(),(0* n),f,g #) is right_complementable
proof
let v be Element of RLSMetrStruct(# (REAL 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),(),(0* n),f,g #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. RLSMetrStruct(# (REAL n),(),(0* n),f,g #)
thus v + w = v1 - v1 by A1
.= 0. RLSMetrStruct(# (REAL n),(),(0* n),f,g #) by RVSUM_1:37 ; :: thesis: verum
end;
A13: now :: thesis: ( ( for a1 being Real
for v, w being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds a1 * (v + w) = (a1 * v) + (a1 * w) ) & ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v) ) & ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds 1 * v = v ) )
hereby :: thesis: ( ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v) ) & ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds 1 * v = v ) )
let a1 be Real; :: thesis: for v, w being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds a1 * (v + w) = (a1 * v) + (a1 * w)
let v, w be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: a1 * (v + w) = (a1 * v) + (a1 * w)
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: verum
end;
hereby :: thesis: ( ( for a1, b1 being Real
for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds 1 * v = v ) )
let a1, b1 be Real; :: thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v)
let v be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: (a1 + b1) * v = (a1 * v) + (b1 * v)
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: verum
end;
hereby :: thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds 1 * v = v
let a1, b1 be Real; :: thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v)
let v be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: (a1 * b1) * v = a1 * (b1 * v)
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: verum
end;
hereby :: thesis: verum
let v be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: 1 * v = v
reconsider v1 = v as Element of n -tuples_on REAL ;
thus 1 * v = 1 * v1 by A3
.= v by RVSUM_1:52 ; :: thesis: verum
end;
end;
A14: now :: thesis: for a, b, c being VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #) holds
( ( dist (a,b) = 0 implies a = b ) & dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
let a, b, c be VECTOR of RLSMetrStruct(# (REAL n),(),(0* n),f,g #); :: thesis: ( ( dist (a,b) = 0 implies a = b ) & dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
reconsider a1 = a, b1 = b, c1 = c as Element of REAL n ;
thus ( dist (a,b) = 0 implies a = b ) :: thesis: ( dist (a,a) = 0 & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
proof
assume dist (a,b) = 0 ; :: thesis: a = b
then (Pitag_dist n) . (a,b) = 0 by METRIC_1:def 1;
then |.(a1 - b1).| = 0 by EUCLID:def 6;
hence a = b by EUCLID:16; :: thesis: verum
end;
A15: dist (a,c) = () . (a,c) by METRIC_1:def 1
.= |.(a1 - c1).| by EUCLID:def 6 ;
|.(a1 - a1).| = 0 ;
then (Pitag_dist n) . (a,a) = 0 by EUCLID:def 6;
hence dist (a,a) = 0 by METRIC_1:def 1; :: thesis: ( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
thus dist (a,b) = () . (a,b) by METRIC_1:def 1
.= |.(a1 - b1).| by EUCLID:def 6
.= |.(b1 - a1).| by EUCLID:18
.= () . (b,a) by EUCLID:def 6
.= dist (b,a) by METRIC_1:def 1 ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
A16: dist (b,c) = () . (b,c) by METRIC_1:def 1
.= |.(b1 - c1).| by EUCLID:def 6 ;
dist (a,b) = () . (a,b) by METRIC_1:def 1
.= |.(a1 - b1).| by EUCLID:def 6 ;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by ; :: thesis: verum
end;
reconsider RLSMS = RLSMetrStruct(# (REAL n),(),(0* n),f,g #) as non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict RLSMetrStruct by ;
reconsider RLSMS = RLSMS as strict RealLinearMetrSpace by ;
take RLSMS ; :: thesis: ( the carrier of RLSMS = REAL n & the distance of RLSMS = Pitag_dist n & 0. RLSMS = 0* n & ( for x, y being Element of REAL n holds the addF of RLSMS . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of RLSMS . (r,x) = r * x ) )

thus ( the carrier of RLSMS = REAL n & the distance of RLSMS = Pitag_dist n & 0. RLSMS = 0* n & ( for x, y being Element of REAL n holds the addF of RLSMS . (x,y) = x + y ) & ( for x being Element of REAL n
for r being Element of REAL holds the Mult of RLSMS . (r,x) = r * x ) ) by A1, A3; :: thesis: verum