let n be Element of NAT ; :: thesis: for r being real number
for y being Point of (TOP-REAL n) st y in Sphere (0. (TOP-REAL n)),r holds
|.y.| = r
let r be real number ; :: thesis: for y being Point of (TOP-REAL n) st y in Sphere (0. (TOP-REAL n)),r holds
|.y.| = r
let y be Point of (TOP-REAL n); :: thesis: ( y in Sphere (0. (TOP-REAL n)),r implies |.y.| = r )
assume y in Sphere (0. (TOP-REAL n)),r ; :: thesis: |.y.| = r
then |.(y - (0. (TOP-REAL n))).| = r by Th9;
hence |.y.| = r by RLVECT_1:26, RLVECT_1:27; :: thesis: verum