theorem :: SEQ_4:70

for n being Nat
for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2 ;