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

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