let i be Nat; :: thesis: for R1, R2 being i -element FinSequence of COMPLEX st R1 - R2 = i |-> 0c holds
R1 = R2
let R1, R2 be i -element FinSequence of COMPLEX ; :: thesis: ( R1 - R2 = i |-> 0c implies R1 = R2 )
assume R1 - R2 = i |-> 0c ; :: thesis: R1 = R2
then R1 = - (- R2) by BINOP_2:1, FINSEQOP:74, SEQ_4:51, SEQ_4:52;
hence R1 = R2 ; :: thesis: verum