let V1, V2 be strict RealLinearMetrSpace; :: thesis: ( the carrier of V1 = REAL n & the distance of V1 = Pitag_dist n & 0. V1 = 0* n & ( for x, y being Element of REAL n holds the addF of V1 . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of V1 . (r,x) = r * x ) & the carrier of V2 = REAL n & the distance of V2 = Pitag_dist n & 0. V2 = 0* n & ( for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of V2 . (r,x) = r * x ) implies V1 = V2 )

assume that

A17: the carrier of V1 = REAL n and

A18: ( the distance of V1 = Pitag_dist n & 0. V1 = 0* n ) and

A19: for x, y being Element of REAL n holds the addF of V1 . (x,y) = x + y and

A20: for x being Element of REAL n

for r being Element of REAL holds the Mult of V1 . (r,x) = r * x and

A21: the carrier of V2 = REAL n and

A22: ( the distance of V2 = Pitag_dist n & 0. V2 = 0* n ) and

A23: for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y and

A24: for x being Element of REAL n

for r being Element of REAL holds the Mult of V2 . (r,x) = r * x ; :: thesis: V1 = V2

for r being Element of REAL holds the Mult of V1 . (r,x) = r * x ) & the carrier of V2 = REAL n & the distance of V2 = Pitag_dist n & 0. V2 = 0* n & ( for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y ) & ( for x being Element of REAL n

for r being Element of REAL holds the Mult of V2 . (r,x) = r * x ) implies V1 = V2 )

assume that

A17: the carrier of V1 = REAL n and

A18: ( the distance of V1 = Pitag_dist n & 0. V1 = 0* n ) and

A19: for x, y being Element of REAL n holds the addF of V1 . (x,y) = x + y and

A20: for x being Element of REAL n

for r being Element of REAL holds the Mult of V1 . (r,x) = r * x and

A21: the carrier of V2 = REAL n and

A22: ( the distance of V2 = Pitag_dist n & 0. V2 = 0* n ) and

A23: for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y and

A24: for x being Element of REAL n

for r being Element of REAL holds the Mult of V2 . (r,x) = r * x ; :: thesis: V1 = V2

now :: thesis: for x, y being Element of V1 holds the addF of V1 . (x,y) = the addF of V2 . (x,y)

then A25:
the addF of V1 = the addF of V2
by A17, A21, BINOP_1:2;let x, y be Element of V1; :: thesis: the addF of V1 . (x,y) = the addF of V2 . (x,y)

reconsider x1 = x, y1 = y as Element of REAL n by A17;

thus the addF of V1 . (x,y) = x1 + y1 by A19

.= the addF of V2 . (x,y) by A23 ; :: thesis: verum

end;reconsider x1 = x, y1 = y as Element of REAL n by A17;

thus the addF of V1 . (x,y) = x1 + y1 by A19

.= the addF of V2 . (x,y) by A23 ; :: thesis: verum

now :: thesis: for r being Element of REAL

for x being Element of V1 holds the Mult of V1 . (r,x) = the Mult of V2 . (r,x)

hence
V1 = V2
by A17, A18, A21, A22, A25, BINOP_1:2; :: thesis: verumfor x being Element of V1 holds the Mult of V1 . (r,x) = the Mult of V2 . (r,x)

let r be Element of REAL ; :: thesis: for x being Element of V1 holds the Mult of V1 . (r,x) = the Mult of V2 . (r,x)

let x be Element of V1; :: thesis: the Mult of V1 . (r,x) = the Mult of V2 . (r,x)

reconsider x1 = x as Element of REAL n by A17;

thus the Mult of V1 . (r,x) = r * x1 by A20

.= the Mult of V2 . (r,x) by A24 ; :: thesis: verum

end;let x be Element of V1; :: thesis: the Mult of V1 . (r,x) = the Mult of V2 . (r,x)

reconsider x1 = x as Element of REAL n by A17;

thus the Mult of V1 . (r,x) = r * x1 by A20

.= the Mult of V2 . (r,x) by A24 ; :: thesis: verum