theorem Th35: :: EUCLID_2:37

for n being Nat
for p being Point of (TOP-REAL n) holds |.p.| = sqrt |(p,p)|