let a, b, s be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = (a . n) + (b . n) ) & ( for k being Nat holds b . k = - (a . (k + 1)) ) implies for n being Nat holds (Partial_Sums s) . n = (a . 0) + (b . n) )
assume that
Z1: for n being Nat holds s . n = (a . n) + (b . n) and
Z2: for k being Nat holds b . k = - (a . (k + 1)) ; :: thesis: for n being Nat holds (Partial_Sums s) . n = (a . 0) + (b . n)
let n be Nat; :: thesis: (Partial_Sums s) . n = (a . 0) + (b . n)
defpred S₁[ Nat] means (Partial_Sums s) . $1 = (a . 0) + (b . $1);
(Partial_Sums s) . 0 = s . 0 by SERIES_1:def 1
.= (a . 0) + (b . 0) by Z1 ;
then A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then (Partial_Sums s) . (k + 1) = ((a . 0) + (b . k)) + (s . (k + 1)) by SERIES_1:def 1
.= ((a . 0) + (b . k)) + ((a . (k + 1)) + (b . (k + 1))) by Z1
.= ((a . 0) + (- (a . (k + 1)))) + ((a . (k + 1)) + (b . (k + 1))) by Z2
.= (a . 0) + (b . (k + 1)) ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence (Partial_Sums s) . n = (a . 0) + (b . n) ; :: thesis: verum