let s be Real_Sequence; :: thesis: ( s is summable implies for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) )
defpred S₁[ Element of NAT ] means Sum s = ((Partial_Sums s) . $1) + (Sum (s ^\ ($1 + 1)));
assume A1: s is summable ; :: thesis: for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1)))
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) ; :: thesis: S₁[n + 1]
reconsider s1 = NAT --> ((s ^\ (n + 1)) . 0 ) as Real_Sequence ;
for k being Element of NAT holds s1 . k = (s ^\ (n + 1)) . 0 by FUNCOP_1:13;
then A4: Partial_Sums ((s ^\ (n + 1)) ^\ 1) = ((Partial_Sums (s ^\ (n + 1))) ^\ 1) - s1 by Th14;
s ^\ (n + 1) is summable by A1, Th15;
then A5: Partial_Sums (s ^\ (n + 1)) is convergent by Def2;
lim (Partial_Sums (s ^\ ((n + 1) + 1))) = lim (Partial_Sums ((s ^\ (n + 1)) ^\ 1)) by NAT_1:49
.= (lim ((Partial_Sums (s ^\ (n + 1))) ^\ 1)) - (lim s1) by A5, A4, SEQ_2:26
.= (lim (Partial_Sums (s ^\ (n + 1)))) - (lim s1) by A5, SEQ_4:33
.= (Sum (s ^\ (n + 1))) - (s1 . 0 ) by SEQ_4:41
.= (Sum (s ^\ (n + 1))) - ((s ^\ (n + 1)) . 0 ) by FUNCOP_1:13 ;
then Sum (s ^\ ((n + 1) + 1)) = (Sum s) - (((Partial_Sums s) . n) + ((s ^\ (n + 1)) . 0 )) by A3
.= (Sum s) - (((Partial_Sums s) . n) + (s . (0 + (n + 1)))) by NAT_1:def 3
.= (Sum s) - ((Partial_Sums s) . (n + 1)) by Def1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

reconsider s1 = NAT --> (s . 0 ) as Real_Sequence ;
A7: Partial_Sums s is convergent by A1, Def2;
for k being Element of NAT holds s1 . k = s . 0 by FUNCOP_1:13;
then Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by Th14;
then lim (Partial_Sums (s ^\ 1)) = (lim ((Partial_Sums s) ^\ 1)) - (lim s1) by A7, SEQ_2:26
.= (lim (Partial_Sums s)) - (lim s1) by A7, SEQ_4:33
.= (Sum s) - (s1 . 0 ) by SEQ_4:41
.= (Sum s) - (s . 0 ) by FUNCOP_1:13 ;
then Sum s = (Sum (s ^\ 1)) + (- (- (s . 0 ))) ;
hence S₁[ 0 ] by Def1; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A2); :: thesis: verum