let f be Real_Sequence; :: thesis: for n being Nat st f . 0 = 0 holds
Sum (FinSeq (f,n)) = (Partial_Sums f) . n
let n be Nat; :: thesis: ( f . 0 = 0 implies Sum (FinSeq (f,n)) = (Partial_Sums f) . n )
assume A0: f . 0 = 0 ; :: thesis: Sum (FinSeq (f,n)) = (Partial_Sums f) . n
defpred S₁[ Nat] means Sum (FinSeq (f,$1)) = (Partial_Sums f) . $1;
Sum (FinSeq (f,0)) = 0
.= (Partial_Sums f) . 0 by A0, SERIES_1:def 1 ;
then A1: S₁[ 0 ] ;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
A4: (FinSeq (f,i)) ^ <*(f . (i + 1))*> = FinSeq (f,(i + 1)) by Th20;
(Partial_Sums f) . (i + 1) = ((Partial_Sums f) . i) + (f . (i + 1)) by SERIES_1:def 1
.= (addreal "**" (FinSeq (f,i))) + (f . (i + 1)) by RVSUM_1:def 12, A3
.= addreal . ((addreal "**" (FinSeq (f,i))),(f . (i + 1))) by BINOP_2:def 9
.= addreal "**" ((FinSeq (f,i)) ^ <*(f . (i + 1))*>) by FINSOP_1:4
.= Sum (FinSeq (f,(i + 1))) by RVSUM_1:def 12, A4 ;
hence S₁[i + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence Sum (FinSeq (f,n)) = (Partial_Sums f) . n ; :: thesis: verum