theorem Th41: :: EUCLID_3:41

for p, q being Point of (TOP-REAL 2) holds |(p,q)| = ((p `1) * (q `1)) + ((p `2) * (q `2))