reconsider j = 1 as non negative Real ;
let n be non zero Element of NAT ; :: thesis: for x being Point of (TOP-REAL n) st x is Point of (Tunit_circle n) holds
|.x.| = 1
let x be Point of (TOP-REAL n); :: thesis: ( x is Point of (Tunit_circle n) implies |.x.| = 1 )
assume x is Point of (Tunit_circle n) ; :: 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