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
A18: the carrier of V1 = REAL n and
A19: the distance of V1 = Pitag_dist n and
A20: 0. V1 = 0* n and
A21: for x, y being Element of REAL n holds the addF of V1 . x,y = x + y and
A22: for x being Element of REAL n
for r being Element of REAL holds the Mult of V1 . r,x = r * x and
A23: the carrier of V2 = REAL n and
A24: the distance of V2 = Pitag_dist n and
A25: 0. V2 = 0* n and
A26: for x, y being Element of REAL n holds the addF of V2 . x,y = x + y and
A27: 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 A18;
thus the addF of V1 . x,y = x1 + y1 by A21
.= the addF of V2 . x,y by A26 ; :: thesis: verum

end;

then A28: the addF of V1 = the addF of V2 by A18, A23, 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 A18;
thus the Mult of V1 . r,x = r * x1 by A22
.= the Mult of V2 . r,x by A27 ; :: thesis: verum

end;

hence V1 = V2 by A18, A19, A20, A23, A24, A25, A28, BINOP_1:2; :: thesis: verum