let a be Real_Sequence; :: thesis: for n being Nat st ( for k being Nat st k <= n holds
a . k = 0 ) holds
(Partial_Sums a) . n = 0
defpred S₁[ Nat] means ( ( for k being Nat st k <= $1 holds
a . k = 0 ) implies (Partial_Sums a) . $1 = 0 );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now :: thesis: ( ( for k being Nat st k <= n + 1 holds
a . k = 0 ) implies (Partial_Sums a) . (n + 1) = 0 )

assume A3: for k being Nat st k <= n + 1 holds
a . k = 0 ; :: thesis: (Partial_Sums a) . (n + 1) = 0

A4: now :: thesis: for k being Nat st k <= n holds
a . k = 0

A5: n <= n + 1 by NAT_1:11;
let k be Nat; :: thesis: ( k <= n implies a . k = 0 )
assume k <= n ; :: thesis: a . k = 0
hence a . k = 0 by A3, A5, XXREAL_0:2; :: thesis: verum

end;

thus (Partial_Sums a) . (n + 1) = ((Partial_Sums a) . n) + (a . (n + 1)) by SERIES_1:def 1
.= 0 by A2, A3, A4 ; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

assume for k being Nat st k <= 0 holds
a . k = 0 ; :: thesis: (Partial_Sums a) . 0 = 0
then a . 0 = 0 ;
hence (Partial_Sums a) . 0 = 0 by SERIES_1:def 1; :: thesis: verum

end;

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