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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) ; :: thesis: S₁[n + 1]
set s1 = seq_const ((s ^\ (n + 1)) . 0);
for k being Nat holds (seq_const ((s ^\ (n + 1)) . 0)) . k = (s ^\ (n + 1)) . 0 by SEQ_1:57;
then A4: Partial_Sums ((s ^\ (n + 1)) ^\ 1) = ((Partial_Sums (s ^\ (n + 1))) ^\ 1) - (seq_const ((s ^\ (n + 1)) . 0)) by Th11;
s ^\ (n + 1) is summable by A1, Th12;
then A5: Partial_Sums (s ^\ (n + 1)) is convergent ;
lim (Partial_Sums (s ^\ ((n + 1) + 1))) = lim (Partial_Sums ((s ^\ (n + 1)) ^\ 1)) by NAT_1:48
.= (lim ((Partial_Sums (s ^\ (n + 1))) ^\ 1)) - (lim (seq_const ((s ^\ (n + 1)) . 0))) by A5, A4, SEQ_2:12
.= (lim (Partial_Sums (s ^\ (n + 1)))) - (lim (seq_const ((s ^\ (n + 1)) . 0))) by A5, SEQ_4:20
.= (Sum (s ^\ (n + 1))) - ((seq_const ((s ^\ (n + 1)) . 0)) . 0) by SEQ_4:26
.= (Sum (s ^\ (n + 1))) - ((s ^\ (n + 1)) . 0) by SEQ_1:57 ;
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

set s1 = seq_const (s . 0);
A7: Partial_Sums s is convergent by A1;
for k being Nat holds (seq_const (s . 0)) . k = s . 0 by SEQ_1:57;
then Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - (seq_const (s . 0)) by Th11;
then lim (Partial_Sums (s ^\ 1)) = (lim ((Partial_Sums s) ^\ 1)) - (lim (seq_const (s . 0))) by A7, SEQ_2:12
.= (lim (Partial_Sums s)) - (lim (seq_const (s . 0))) by A7, SEQ_4:20
.= (Sum s) - ((seq_const (s . 0)) . 0) by SEQ_4:26
.= (Sum s) - (s . 0) by SEQ_1:57 ;
then Sum s = (Sum (s ^\ 1)) + (- (- (s . 0))) ;
hence S₁[ 0 ] by Def1; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A2); :: thesis: verum