theorem Th50: :: EUCLID_8:59
for x, y, z, r being Real holds r * |[x,y,z]| = |[(r * x),(r * y),(r * z)]|