theorem :: POLYNOM5:11

for x, y, z being Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>