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

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