let i be Nat; :: thesis: for R1, R, R2 being i -long FinSequence of COMPLEX st R1 + R = R2 + R holds
R1 = R2
let R1, R, R2 be i -long FinSequence of COMPLEX ; :: thesis: ( R1 + R = R2 + R implies R1 = R2 )
assume R1 + R = R2 + R ; :: thesis: R1 = R2
then R1 + (R + (- R)) = (R2 + R) + (- R) by FINSEQOP:29;
then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by FINSEQOP:29;
R + (- R) = i |-> 0c by SEQ_4:68, SEQ_4:69, BINOP_2:1, FINSEQOP:77;
then R1 = R2 + (i |-> 0c) by A1, BINOP_2:1, FINSEQOP:57;
hence R1 = R2 by BINOP_2:1, FINSEQOP:57; :: thesis: verum