let a be Real_Sequence; :: thesis: for n being Nat st ( for k being Nat st k <= n holds
a . k = 0 ) holds
() . n = 0

defpred S1[ Nat] means ( ( for k being Nat st k <= \$1 holds
a . k = 0 ) implies () . \$1 = 0 );
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: ( ( for k being Nat st k <= n + 1 holds
a . k = 0 ) implies () . (n + 1) = 0 )
assume A3: for k being Nat st k <= n + 1 holds
a . k = 0 ; :: thesis: () . (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 ; :: thesis: verum
end;
thus () . (n + 1) = (() . n) + (a . (n + 1)) by SERIES_1:def 1
.= 0 by A2, A3, A4 ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A6: S1[ 0 ]
proof
assume for k being Nat st k <= 0 holds
a . k = 0 ; :: thesis: () . 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 S1[n] from NAT_1:sch 2(A6, A1); :: thesis: verum