theorem :: COMPLFLD:11

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