let n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds
z1 = z2
let z1, z2 be Element of COMPLEX n; :: thesis: ( z1 - z2 = 0c n implies z1 = z2 )
assume z1 - z2 = 0c n ; :: thesis: z1 = z2
then z1 + (- z2) = 0c n ;
then z1 = - (- z2) by Th51, Th52, BINOP_2:1, FINSEQOP:74;
hence z1 = z2 ; :: thesis: verum