let f be Real_Sequence; :: thesis: ( ex n being Nat st
for k being Nat st k >= n holds
f . k = 0 implies ex n being Nat st
for k being Nat st k >= n holds
(Partial_Sums f) . k = (Partial_Sums f) . n )
given n being Nat such that A1: for k being Nat st k >= n holds
f . k = 0 ; :: thesis: ex n being Nat st
for k being Nat st k >= n holds
(Partial_Sums f) . k = (Partial_Sums f) . n
set p = Partial_Sums f;
reconsider pk = (Partial_Sums f) . n as Real ;
set r = seq_const pk;
A2: for k being Nat st k >= n holds
(Partial_Sums f) . k = (seq_const pk) . k

proof

let k be Nat; :: thesis: ( k >= n implies (Partial_Sums f) . k = (seq_const pk) . k )
assume A3: k >= n ; :: thesis: (Partial_Sums f) . k = (seq_const pk) . k
defpred S₁[ Nat] means (Partial_Sums f) . $1 = (seq_const pk) . $1;
A4: S₁[n] by SEQ_1:57;
A5: for i being Nat st n <= i & S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( n <= i & S₁[i] implies S₁[i + 1] )
assume A6: n <= i ; :: thesis: ( not S₁[i] or S₁[i + 1] )
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
(Partial_Sums f) . (i + 1) = ((Partial_Sums f) . i) + (f . (i + 1)) by SERIES_1:def 1
.= ((seq_const pk) . i) + 0 by A1, A6, A7, NAT_1:12
.= pk by SEQ_1:57
.= (seq_const pk) . (i + 1) ;
hence S₁[i + 1] ; :: thesis: verum

end;

for k being Nat st n <= k holds
S₁[k] from NAT_1:sch 8(A4, A5);
hence (Partial_Sums f) . k = (seq_const pk) . k by A3; :: thesis: verum

end;

take n ; :: thesis: for k being Nat st k >= n holds
(Partial_Sums f) . k = (Partial_Sums f) . n
let k be Nat; :: thesis: ( k >= n implies (Partial_Sums f) . k = (Partial_Sums f) . n )
assume k >= n ; :: thesis: (Partial_Sums f) . k = (Partial_Sums f) . n
then (Partial_Sums f) . k = (seq_const pk) . k by A2
.= (Partial_Sums f) . n by SEQ_1:57 ;
hence (Partial_Sums f) . k = (Partial_Sums f) . n ; :: thesis: verum