theorem :: POLYNOM5:11

for x, y, z being Element of F_Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>