let n be Nat; :: thesis: for cF being complex-valued XFinSequence st n in dom cF holds
(Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1))
let cF be complex-valued XFinSequence; :: thesis: ( n in dom cF implies (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) )
assume A1: n in dom cF ; :: thesis: (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1))
reconsider cF = cF as XFinSequence of COMPLEX ;
addcomplex . ((addcomplex "**" (cF | n)),(cF . n)) = addcomplex "**" (cF | (n + 1)) by Th42, A1;
hence (Sum (cF | n)) + (cF . n) = Sum (cF | (n + 1)) by BINOP_2:def 3; :: thesis: verum