theorem :: REAL_NS1:14

for n being Nat
for x1 being Point of (REAL-NS n)
for x2 being Point of (REAL-US n) st x1 = x2 holds
||.x1.|| ^2 = x2 .|. x2