theorem :: EUCLID_8:66

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