theorem Th71: :: SEQ_4:72
for n being Nat
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2