let r be Complex; :: thesis: OddEvenPowers (r,1) = <*1*>
A1: len (OddEvenPowers (r,1)) = 1 by Def3;
(OddEvenPowers (r,1)) . ((2 * 0) + 1) = r |^ (1 - 1) by Def3;
hence OddEvenPowers (r,1) = <*1*> by A1, FINSEQ_1:40, NEWTON:4; :: thesis: verum