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