theorem Th78: :: SEQ_4:79

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