let n be non zero Nat; :: thesis: odd-seq (n + 1) = (odd-seq n) ^ <*((2 * n) + 1)*>
n < n + 1 by NAT_1:16;
then A5: n < len (odd-seq (n + 1)) by Th1;
A2: (odd-seq (n + 1)) | (n + 1) = (odd-seq (n + 1)) | (dom (odd-seq (n + 1))) by Th1
.= odd-seq (n + 1) ;
A3: (odd-seq (n + 1)) | n = odd-seq n by Th6;
A4: dom (odd-seq (n + 1)) = Seg (n + 1) by Th1;
A6: dom (even-seq (n + 1)) = Seg (len (even-seq (n + 1))) by FINSEQ_1:def 3
.= Seg (n + 1) by Def1 ;
then A7: ((dom (even-seq (n + 1))) --> (- 1)) . (n + 1) = - 1 by FUNCOP_1:7, FINSEQ_1:4;
(odd-seq (n + 1)) . (n + 1) = ((even-seq (n + 1)) . (n + 1)) + (((dom (even-seq (n + 1))) --> (- 1)) . (n + 1)) by FINSEQ_1:4, A4, VALUED_1:def 1
.= (2 * (n + 1)) - 1 by A6, FINSEQ_1:4, A7, Def1
.= (2 * n) + 1 ;
hence odd-seq (n + 1) = (odd-seq n) ^ <*((2 * n) + 1)*> by A3, A2, A5, FINSEQ_5:83; :: thesis: verum