let n be Nat; :: thesis: for z, z1, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
let z, z1, 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:28;
then A1: z1 + (z + (- z)) = z2 + (z + (- z)) by FINSEQOP:28;
z + (- z) = 0c n by Th51, Th52, BINOP_2:1, FINSEQOP:73;
then z1 = z2 + (0c n) by A1, BINOP_2:1, FINSEQOP:56;
hence z1 = z2 by BINOP_2:1, FINSEQOP:56; :: thesis: verum