theorem :: COMPLFLD:51

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