for X being NormedLinearTopSpace
for RNS being RealNormSpace st RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) holds
for x, y being Point of X
for x1, y1 being Point of RNS
for a being Real st x1 = x & y1 = y holds
( x + y = x1 + y1 & a * x = a * x1 & x - y = x1 - y1 & ||.x.|| = ||.x1.|| )