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
A16: the carrier of V1 = REAL n and
A17: ( the distance of V1 = Pitag_dist n & 0. V1 = 0* n ) and
A18: for x, y being Element of REAL n holds the addF of V1 . (x,y) = x + y and
A19: for x being Element of REAL n
for r being Element of REAL holds the Mult of V1 . (r,x) = r * x and
A20: the carrier of V2 = REAL n and
A21: ( the distance of V2 = Pitag_dist n & 0. V2 = 0* n ) and
A22: for x, y being Element of REAL n holds the addF of V2 . (x,y) = x + y and
A23: 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

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 A16;
thus the addF of V1 . (x,y) = x1 + y1 by A18
.= the addF of V2 . (x,y) by A22 ; :: thesis: verum

end;

then A24: the addF of V1 = the addF of V2 by A16, A20, BINOP_1:2;

now

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 A16;
thus the Mult of V1 . (r,x) = r * x1 by A19
.= the Mult of V2 . (r,x) by A23 ; :: thesis: verum

end;

hence V1 = V2 by A16, A17, A20, A21, A24, BINOP_1:2; :: thesis: verum