let k be Nat; :: thesis: for r being Real holds Sum (OddEvenPowers (r,((2 * k) + 3))) = ((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1))))
let r be Real; :: thesis: Sum (OddEvenPowers (r,((2 * k) + 3))) = ((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1))))
A1: OddEvenPowers (r,((2 * (k + 1)) + 1)) = <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> ^ (OddEvenPowers (r,((2 * k) + 1))) by Th19;
Sum <*(r |^ ((2 * k) + 2)),(- (r |^ ((2 * k) + 1)))*> = (r |^ ((2 * k) + 2)) + (- (r |^ ((2 * k) + 1))) by RVSUM_1:77;
hence Sum (OddEvenPowers (r,((2 * k) + 3))) = ((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1)))) by A1, RVSUM_1:75; :: thesis: verum