let i be Nat; :: thesis: for R, R1, R2 being i -element complex-valued FinSequence st R1 + R = R2 + R holds
R1 = R2
let R, R1, R2 be i -element complex-valued FinSequence; :: thesis: ( R1 + R = R2 + R implies R1 = R2 )
A0: ( R is i -element FinSequence of COMPLEX & R1 is i -element FinSequence of COMPLEX & R2 is i -element FinSequence of COMPLEX ) by FINSEQ_1:102;
assume R1 + R = R2 + R ; :: thesis: R1 = R2
then R1 + (R + (- R)) = (R2 + R) + (- R) by A0, FINSEQOP:28;
then A1: R1 + (R + (- R)) = R2 + (R + (- R)) by A0, FINSEQOP:28;
R + (- R) = i |-> 0c by A0, BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52;
then R1 = R2 + (i |-> 0c) by A0, A1, BINOP_2:1, FINSEQOP:56;
hence R1 = R2 by A0, BINOP_2:1, FINSEQOP:56; :: thesis: verum