set F = OddEvenPowers (r,n);
let y be object ; :: according to RELAT_1:def 19,TARSKI:def 3 :: thesis: ( not y in rng (OddEvenPowers (r,n)) or y in INT )
assume y in rng (OddEvenPowers (r,n)) ; :: thesis: y in INT
then consider i being object such that
A1: i in dom (OddEvenPowers (r,n)) and
A2: (OddEvenPowers (r,n)) . i = y by FUNCT_1:def 3;
reconsider i = i as Element of NAT by A1;
A3: len (OddEvenPowers (r,n)) = n by Def3;
A4: ( 1 <= i & i <= len (OddEvenPowers (r,n)) ) by A1, FINSEQ_3:25;
then reconsider m = n - i as Element of NAT by A3, INT_1:5;
( ( i is odd implies (OddEvenPowers (r,n)) . i = r |^ m ) & ( i is even implies (OddEvenPowers (r,n)) . i = - (r |^ m) ) ) by A3, A4, Def3;
hence y in INT by A2, INT_1:def 2; :: thesis: verum