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