let r be Complex; :: thesis: Sum (OddEvenPowers (r,1)) = 1
OddEvenPowers (r,1) = <*1*> by Th17;
hence Sum (OddEvenPowers (r,1)) = 1 by RVSUM_1:73; :: thesis: verum