theorem :: COMPLFLD:54

for z1, z2 being Element of F_Complex holds (z1 * z2) *' = (z1 *') * (z2 *') by COMPLEX1:35;