theorem Th56: :: EUCLID_8:65

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