let V1, V2 be strict RealLinearMetrSpace; ( 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
; V1 = V2
then A25:
the addF of V1 = the addF of V2
by A17, A21, BINOP_1:2;
hence
V1 = V2
by A17, A18, A21, A22, A25, BINOP_1:2; verum