theorem :: TOPREAL9:12

for n being Nat
for r being Real
for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds
|.y.| = r