theorem Th32: :: EUCLID_8:40

for r, x, y, z being Real holds r * |[x,y,z]| = (((r * x) * <e1>) + ((r * y) * <e2>)) + ((r * z) * <e3>)