theorem Th1: :: REAL_NS1:1

for n being Nat
for x being VECTOR of (REAL-NS n)
for y being Element of REAL n st x = y holds
||.x.|| = |.y.|