for i, n being Nat
for A being non empty closed_interval Subset of REAL holds integral ((((- 1) |^ i) (#) ((#Z (2 * n)) / ((#Z 0) + (#Z 2)))),A) = (((- 1) |^ i) * (((1 / ((2 * n) + 1)) * ((upper_bound A) |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * ((lower_bound A) |^ ((2 * n) + 1))))) + (integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))