let i be Nat; :: thesis: for R being i -element complex-valued FinSequence holds R - (i |-> 0c) = R
let R be i -element complex-valued FinSequence; :: thesis: R - (i |-> 0c) = R
A1: R is i -element FinSequence of COMPLEX by FINSEQ_1:102;
thus R - (i |-> 0c) = R + (i |-> (- 0)) by Th8
.= R by A1, BINOP_2:1, FINSEQOP:56 ; :: thesis: verum