theorem :: COMPLFLD:53

for z1, z2 being Element of F_Complex holds (z1 - z2) *' = (z1 *') - (z2 *')