theorem :: SERIES_4:24

for s being Real_Sequence st ( for n being Nat st n >= 1 holds
( s . n = (2 |^ n) * (((3 * n) - 1) / 4) & s . 0 = 0 ) ) holds
for n being Nat st n >= 1 holds
(Partial_Sums s) . n = ((2 |^ n) * (((3 * n) - 4) / 2)) + 2