theorem :: POLYNOM5:10

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