deffunc H_{1}( Real, Element of REAL n) -> Element of REAL n = $1 * $2;

deffunc H_{2}( 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_{2}(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_{1}(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_{1}(r,x)

reconsider RLSMS = RLSMS as strict RealLinearMetrSpace by A14, A7, A10, Def5, Def6, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4;

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

deffunc H

consider f being BinOp of (REAL n) such that

A1: for x, y being Element of REAL n holds f . (x,y) = H

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

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

proof

let r be Real; :: thesis: for x being Element of REAL n holds g . (r,x) = H_{1}(r,x)

let x be Element of REAL n; :: thesis: g . (r,x) = H_{1}(r,x)

reconsider r = r as Element of REAL by XREAL_0:def 1;

g . (r,x) = H_{1}(r,x)
by A2;

hence g . (r,x) = H_{1}(r,x)
; :: thesis: verum

end;let x be Element of REAL n; :: thesis: g . (r,x) = H

reconsider r = r as Element of REAL by XREAL_0:def 1;

g . (r,x) = H

hence g . (r,x) = H

A4: now :: thesis: for u, v, w being Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (u + v) + w = u + (v + w)

let u, v, w be Element of RLSMetrStruct(# (REAL n),(Pitag_dist 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;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

A5: now :: thesis: for v, w being Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds v + w = w + v

let v, w be Element of RLSMetrStruct(# (REAL n),(Pitag_dist 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;reconsider v1 = v, w1 = w as Element of REAL n ;

thus v + w = v1 + w1 by A1

.= w + v by A1 ; :: thesis: verum

A6: now :: thesis: for v being Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = v

let v be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: thesis: v + (0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)) = v

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: verum

end;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: verum

A7: now :: thesis: for r being Real

for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))

for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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),(Pitag_dist n),(0* n),f,g #) holds dist ((r * v),(r * w)) = |.r.| * (dist (v,w))

let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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) = (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: verum

end;let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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) = (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: verum

A10: now :: thesis: for u, w, v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds dist (v,w) = dist ((v + u),(w + u))

A12:
RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) is right_complementable
let u, w, v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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) = (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: verum

end;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: verum

proof

let v be Element of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

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: v + w = 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)

thus v + w = v1 - v1 by A1

.= 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) by RVSUM_1:37 ; :: thesis: verum

end;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: v + w = 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #)

thus v + w = v1 - v1 by A1

.= 0. RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) by RVSUM_1:37 ; :: thesis: verum

A13: now :: thesis: ( ( for a1 being Real

for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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),(Pitag_dist 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),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )end;

for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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),(Pitag_dist 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),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )

hereby :: thesis: ( ( for a1, b1 being Real

for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )

for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )

let a1 be Real; :: thesis: for v, w being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds a1 * (v + w) = (a1 * v) + (a1 * w)

let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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;let v, w be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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

hereby :: thesis: ( ( for a1, b1 being Real

for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )

for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v) ) & ( for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v ) )

let a1, b1 be Real; :: thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 + b1) * v = (a1 * v) + (b1 * v)

let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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;let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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

hereby :: thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds 1 * v = v

let a1, b1 be Real; :: thesis: for v being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist n),(0* n),f,g #) holds (a1 * b1) * v = a1 * (b1 * v)

let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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;let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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

hereby :: thesis: verum

let v be VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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;reconsider v1 = v as Element of n -tuples_on REAL ;

thus 1 * v = 1 * v1 by A3

.= v by RVSUM_1:52 ; :: thesis: verum

A14: now :: thesis: for a, b, c being VECTOR of RLSMetrStruct(# (REAL n),(Pitag_dist 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)) )

reconsider RLSMS = RLSMetrStruct(# (REAL n),(Pitag_dist 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 A5, A4, A6, A12, A13, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8;( ( 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),(Pitag_dist 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)) )

.= |.(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) = (Pitag_dist n) . (a,b) by METRIC_1:def 1

.= |.(a1 - b1).| by EUCLID:def 6

.= |.(b1 - a1).| by EUCLID:18

.= (Pitag_dist n) . (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) = (Pitag_dist n) . (b,c) by METRIC_1:def 1

.= |.(b1 - c1).| by EUCLID:def 6 ;

dist (a,b) = (Pitag_dist n) . (a,b) by METRIC_1:def 1

.= |.(a1 - b1).| by EUCLID:def 6 ;

hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A15, A16, EUCLID:19; :: thesis: verum

end;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

A15: dist (a,c) =
(Pitag_dist n) . (a,c)
by METRIC_1:def 1
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;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

.= |.(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) = (Pitag_dist n) . (a,b) by METRIC_1:def 1

.= |.(a1 - b1).| by EUCLID:def 6

.= |.(b1 - a1).| by EUCLID:18

.= (Pitag_dist n) . (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) = (Pitag_dist n) . (b,c) by METRIC_1:def 1

.= |.(b1 - c1).| by EUCLID:def 6 ;

dist (a,b) = (Pitag_dist n) . (a,b) by METRIC_1:def 1

.= |.(a1 - b1).| by EUCLID:def 6 ;

hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A15, A16, EUCLID:19; :: thesis: verum

reconsider RLSMS = RLSMS as strict RealLinearMetrSpace by A14, A7, A10, Def5, Def6, METRIC_1:1, METRIC_1:2, METRIC_1:3, METRIC_1:4;

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