let Fr be XFinSequence of REAL ; :: thesis: for n being Element of NAT st n in dom Fr holds
(Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1))
let n be Element of NAT ; :: thesis: ( n in dom Fr implies (Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1)) )
assume A1: n in dom Fr ; :: thesis: (Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1))
( addreal . (addreal "**" (Fr | n)),(Fr . n) = addreal "**" (Fr | (n + 1)) & addreal . (addreal "**" (Fr | n)),(Fr . n) = (addreal "**" (Fr | n)) + (Fr . n) & addreal "**" (Fr | n) = Sum (Fr | n) ) by A1, BINOP_2:def 9, CARD_FIN:42;
hence (Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1)) ; :: thesis: verum