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