let s, s1 be Real_Sequence; :: thesis: ( ( for n being Nat holds s1 . n = s . 0 ) implies Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 )
assume A1: for n being Nat holds s1 . n = s . 0 ; :: thesis: Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1

A2: now :: thesis: for k being Nat holds (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))

let k be Nat; :: thesis: (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1))
thus (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = (((Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1)) by RFUNCT_2:1
.= (((Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0) by A1
.= ((Partial_Sums s) . ((k + 1) + 1)) - (s . 0) by NAT_1:def 3
.= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s . 0) by Def1
.= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s1 . k) by A1
.= (s . ((k + 1) + 1)) + (((Partial_Sums s) . (k + 1)) - (s1 . k))
.= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) . k) - (s1 . k)) by NAT_1:def 3
.= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) - s1) . k) by RFUNCT_2:1
.= ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) by NAT_1:def 3 ; :: thesis: verum

end;

(((Partial_Sums s) ^\ 1) - s1) . 0 = (((Partial_Sums s) ^\ 1) . 0) - (s1 . 0) by RFUNCT_2:1
.= (((Partial_Sums s) ^\ 1) . 0) - (s . 0) by A1
.= ((Partial_Sums s) . (0 + 1)) - (s . 0) by NAT_1:def 3
.= (((Partial_Sums s) . 0) + (s . (0 + 1))) - (s . 0) by Def1
.= ((s . (0 + 1)) + (s . 0)) - (s . 0) by Def1
.= (s ^\ 1) . 0 by NAT_1:def 3 ;
hence Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by A2, Def1; :: thesis: verum