theorem Th21: :: EUCLID_3:21

for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = sqrt (((p `1) ^2) + ((p `2) ^2))