theorem Th12: :: TOPREALB:12

for n being non zero Element of NAT
for x being Point of (TOP-REAL n) st x is Point of (Tunit_circle n) holds
|.x.| = 1