let V1, V2 be strict RealLinearMetrSpace; :: thesis:
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:

let x, y be Element of V1; :: thesis:
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:

end;

let r be Element of REAL ; :: thesis:
let x be Element of V1; :: thesis:
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:

end;