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