let n be Nat; :: thesis: for r being Real holds (r |^ ((2 * n) + 1)) + 1 = (r + 1) * (Sum (OddEvenPowers (r,((2 * n) + 1))))
let r be Real; :: thesis: (r |^ ((2 * n) + 1)) + 1 = (r + 1) * (Sum (OddEvenPowers (r,((2 * n) + 1))))
defpred S₁[ Nat] means (r |^ ((2 * $1) + 1)) + 1 = (r + 1) * (Sum (OddEvenPowers (r,((2 * $1) + 1))));
A1: S₁[ 0 ]

proof

Sum (OddEvenPowers (r,1)) = 1 by Th18;
hence (r |^ ((2 * 0) + 1)) + 1 = (r + 1) * (Sum (OddEvenPowers (r,((2 * 0) + 1)))) ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: Sum (OddEvenPowers (r,((2 * k) + 3))) = ((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1)))) by Th20;
A5: r * (r |^ ((2 * k) + 2)) = r |^ (((2 * k) + 2) + 1) by NEWTON:6;
r * (r |^ ((2 * k) + 1)) = r |^ (((2 * k) + 1) + 1) by NEWTON:6;
then r |^ ((2 * (k + 1)) + 1) = (((r + 1) * (r |^ ((2 * k) + 2))) - ((r + 1) * (r |^ ((2 * k) + 1)))) + (r |^ ((2 * k) + 1)) by A5;
hence (r |^ ((2 * (k + 1)) + 1)) + 1 = (r + 1) * (((r |^ ((2 * k) + 2)) - (r |^ ((2 * k) + 1))) + (Sum (OddEvenPowers (r,((2 * k) + 1))))) by A3
.= (r + 1) * (Sum (OddEvenPowers (r,((2 * (k + 1)) + 1)))) by A4 ;
:: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence (r |^ ((2 * n) + 1)) + 1 = (r + 1) * (Sum (OddEvenPowers (r,((2 * n) + 1)))) ; :: thesis: verum