theorem Th1: :: RUSUB_7:1

for X being RealUnitarySpace
for x, y being Point of X
for z, t being Point of (MetricSpaceNorm (RUSp2RNSp X)) st x = z & y = t holds
||.(x - y).|| = dist (z,t)