theorem Th80: :: SEQ_4:81

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