theorem Th8: :: EUCLID_5:8

for x, x1, y1, z1 being Real holds x * |[x1,y1,z1]| = |[(x * x1),(x * y1),(x * z1)]|