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 A1: n in dom F ; :: thesis: (Sum (F | n)) + (F . n) = Sum (F | (n + 1))
( addnat . (addnat "**" (F | n)),(F . n) = addnat "**" (F | (n + 1)) & addnat . (addnat "**" (F | n)),(F . n) = (addnat "**" (F | n)) + (F . n) & addnat "**" (F | n) = Sum (F | n) ) by A1, Th42, BINOP_2:def 23, STIRL2_1:def 4;
hence (Sum (F | n)) + (F . n) = Sum (F | (n + 1)) by STIRL2_1:def 4; :: thesis: verum