let F be XFinSequence of ; :: thesis: for n being Element of NAT st n in dom F holds
(Sum (F | n)) + (F . n) = Sum (F | (n + 1))
let n be Element of NAT ; :: thesis: ( n in dom F implies (Sum (F | n)) + (F . n) = Sum (F | (n + 1)) )
assume n in dom F ; :: thesis: (Sum (F | n)) + (F . n) = Sum (F | (n + 1))
then A1: addnat . (addnat "**" (F | n)),(F . n) = addnat "**" (F | (n + 1)) by Th42;
( addnat . (addnat "**" (F | n)),(F . n) = (addnat "**" (F | n)) + (F . n) & addnat "**" (F | n) = Sum (F | n) ) by BINOP_2:def 23, STIRL2_1:def 4;
hence (Sum (F | n)) + (F . n) = Sum (F | (n + 1)) by A1, STIRL2_1:def 4; :: thesis: verum