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 n in dom Fr ; :: thesis: (Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1))
then addreal . (addreal "**" (Fr | n)),(Fr . n) = addreal "**" (Fr | (n + 1)) by CARD_FIN:42;
hence (Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1)) by BINOP_2:def 9; :: thesis: verum