let i, k be Nat; :: thesis: for r being Real holds ((Partial_Sums (r GeoSeq)) . ((k + i) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . i)
let r be Real; :: thesis: ((Partial_Sums (r GeoSeq)) . ((k + i) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . i)
set S = r GeoSeq ;
set P = Partial_Sums (r GeoSeq);
defpred S₁[ Nat] means ((Partial_Sums (r GeoSeq)) . ((k + $1) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . $1);
A1: S₁[ 0 ]

proof

A2: (Partial_Sums (r GeoSeq)) . 0 = (r GeoSeq) . 0 by SERIES_1:def 1
.= 1 by PREPOWER:3 ;
(Partial_Sums (r GeoSeq)) . (k + 1) = ((Partial_Sums (r GeoSeq)) . k) + ((r GeoSeq) . (k + 1)) by SERIES_1:def 1;
hence S₁[ 0 ] by A2, PREPOWER:def 1; :: thesis: verum

end;

A3: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume A4: S₁[a] ; :: thesis: S₁[a + 1]
A5: (Partial_Sums (r GeoSeq)) . (a + 1) = ((Partial_Sums (r GeoSeq)) . a) + ((r GeoSeq) . (a + 1)) by SERIES_1:def 1;
A6: (r GeoSeq) . (k + (a + 1)) = ((r GeoSeq) . (a + 1)) * (r |^ k) by Th20;
A7: (r GeoSeq) . ((k + (a + 1)) + 1) = ((r GeoSeq) . (k + (a + 1))) * r by PREPOWER:3
.= ((r GeoSeq) . (a + 1)) * ((r |^ k) * r) by A6
.= (r |^ (k + 1)) * ((r GeoSeq) . (a + 1)) by NEWTON:6 ;
(Partial_Sums (r GeoSeq)) . ((k + (a + 1)) + 1) = ((Partial_Sums (r GeoSeq)) . (k + (a + 1))) + ((r GeoSeq) . ((k + (a + 1)) + 1)) by SERIES_1:def 1;
hence ((Partial_Sums (r GeoSeq)) . ((k + (a + 1)) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (((Partial_Sums (r GeoSeq)) . (k + (a + 1))) - ((Partial_Sums (r GeoSeq)) . k)) + ((r GeoSeq) . ((k + (a + 1)) + 1))
.= ((r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . a)) + ((r GeoSeq) . ((k + (a + 1)) + 1)) by A4
.= (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . (a + 1)) by A5, A7 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A3);
hence ((Partial_Sums (r GeoSeq)) . ((k + i) + 1)) - ((Partial_Sums (r GeoSeq)) . k) = (r |^ (k + 1)) * ((Partial_Sums (r GeoSeq)) . i) ; :: thesis: verum