let n be non zero Nat; :: thesis: for i being Nat st i in dom (odd-seq n) holds
(odd-seq n) . i = (2 * i) - 1
let i be Nat; :: thesis: ( i in dom (odd-seq n) implies (odd-seq n) . i = (2 * i) - 1 )
assume A1: i in dom (odd-seq n) ; :: thesis: (odd-seq n) . i = (2 * i) - 1
then i in Seg n by Th1;
then a2: i in dom (even-seq n) by Th1;
then A3: ((dom (even-seq n)) --> (- 1)) . i = - 1 by FUNCOP_1:7;
(odd-seq n) . i = ((even-seq n) . i) + (((dom (even-seq n)) --> (- 1)) . i) by A1, VALUED_1:def 1
.= (2 * i) - 1 by a2, Def1, A3 ;
hence (odd-seq n) . i = (2 * i) - 1 ; :: thesis: verum