theorem :: SERIES_4:16

for s being Real_Sequence st ( for n being Nat holds s . n = (((1 / 3) |^ n) + (3 |^ n)) |^ 2 ) holds
for n being Nat holds (Partial_Sums s) . n = (((- (((1 / 9) |^ n) / 8)) + ((9 |^ (n + 1)) / 8)) + (2 * n)) + 3