let n be Element of NAT ; :: thesis: for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
let z1, z, z2 be Element of COMPLEX n; :: thesis: ( z1 + z = z2 + z implies z1 = z2 )
assume z1 + z = z2 + z ; :: thesis: z1 = z2
then z1 + (z + (- z)) = (z2 + z) + (- z) by FINSEQOP:29;
then A1: z1 + (z + (- z)) = z2 + (z + (- z)) by FINSEQOP:29;
z + (- z) = 0c n by Th7, Th8, BINOP_2:1, FINSEQOP:77;
then z1 = z2 + (0c n) by A1, BINOP_2:1, FINSEQOP:57;
hence z1 = z2 by BINOP_2:1, FINSEQOP:57; :: thesis: verum