theorem Th55: :: EUCLID_8:64

for p being Element of REAL 3 holds |(p,p)| = (((p . 1) ^2) + ((p . 2) ^2)) + ((p . 3) ^2)