theorem :: COMPLFLD:12

for z, z1 being Element of F_Complex holds z1 = (z1 + z) - z