set F = OddEvenPowers (r,n);
let i be object ; :: according to VALUED_0:def 9 :: thesis: ( not i in dom (OddEvenPowers (r,n)) or not (OddEvenPowers (r,n)) . i is real )
assume A1: i in dom (OddEvenPowers (r,n)) ; :: thesis: (OddEvenPowers (r,n)) . i is real
then reconsider i = i as Element of NAT ;
A2: len (OddEvenPowers (r,n)) = n by Def3;
A3: ( 1 <= i & i <= len (OddEvenPowers (r,n)) ) by A1, FINSEQ_3:25;
then reconsider m = n - i as Element of NAT by A2, INT_1:5;
( ( i is odd implies (OddEvenPowers (r,n)) . i = r |^ m ) & ( i is even implies (OddEvenPowers (r,n)) . i = - (r |^ m) ) ) by A2, A3, Def3;
hence (OddEvenPowers (r,n)) . i is real ; :: thesis: verum