let n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2
let z1, z2 be Element of COMPLEX n; :: thesis: ( - z1 = - z2 implies z1 = z2 )
assume - z1 = - z2 ; :: thesis: z1 = z2
hence z1 = - (- z2)
.= z2 ;
:: thesis: verum