( dom (odd-seq 1) = Seg 1 & dom (even-seq 1) = Seg 1 ) by Th1;
then A2: ( 1 in dom (odd-seq 1) & 1 in dom (even-seq 1) ) ;
then A3: ((dom (even-seq 1)) --> (- 1)) . 1 = - 1 by FUNCOP_1:7;
A4: len (odd-seq 1) = 1 by Th1;
A5: (odd-seq 1) . 1 = ((even-seq 1) . 1) + (((dom (even-seq 1)) --> (- 1)) . 1) by A2, VALUED_1:def 1
.= (2 * 1) - 1 by A2, Def1, A3
.= 1 ;
A6: odd-seq (1 + 1) = (odd-seq 1) ^ <*((2 * 1) + 1)*> by Th7;
odd-seq (2 + 1) = (odd-seq 2) ^ <*((2 * 2) + 1)*> by Th7;
hence ( odd-seq 1 = <*1*> & odd-seq 2 = <*1,3*> & odd-seq 3 = <*1,3,5*> ) by A5, A4, FINSEQ_1:40, A6; :: thesis: verum