theorem :: COMPLFLD:13

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