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
now :: thesis: for x, y being Element of V1 holds the addF of V1 . (x,y) = the addF of V2 . (x,y)
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;
then A25: the addF of V1 = the addF of V2 by ;
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)
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;
hence V1 = V2 by ; :: thesis: verum