reconsider j = 1 as real non negative number ;
let n be non empty Element of NAT ; :: thesis: for x being Point of st x is Point of holds
|.x.| = 1
let x be Point of ; :: thesis: ( x is Point of implies |.x.| = 1 )
assume x is Point of ; :: thesis: |.x.| = 1
then x in the carrier of (Tcircle (0. (TOP-REAL n)),j) ;
then x in Sphere (0. (TOP-REAL n)),1 by Th9;
hence |.x.| = 1 by TOPREAL9:12; :: thesis: verum