let n be non zero Nat; :: thesis: (odd-seq (n + 1)) | (Seg n) = odd-seq n
set X = Seg n;
set ev = even-seq n;
set h = (even-seq n) + ((dom (even-seq n)) --> (- 1));
set h1 = (even-seq (n + 1)) + ((dom (even-seq (n + 1))) --> (- 1));
A1: len (even-seq n) = n by Def1;
A2: dom (even-seq n) = Seg (len (even-seq n)) by FINSEQ_1:def 3
.= Seg n by Def1 ;
A3: dom (even-seq (n + 1)) = Seg (len (even-seq (n + 1))) by FINSEQ_1:def 3
.= Seg (n + 1) by Def1 ;
A4: (even-seq (n + 1)) | (Seg n) = ((even-seq n) ^ <*(2 * (n + 1))*>) | n by Th3
.= even-seq n by A1 ;
min (n,(n + 1)) = n ;
then (dom (even-seq (n + 1))) /\ (Seg n) = dom (even-seq n) by A2, A3, FINSEQ_2:2;
then ((dom (even-seq (n + 1))) --> (- 1)) | (Seg n) = (dom (even-seq n)) --> (- 1) by FUNCOP_1:12;
hence (odd-seq (n + 1)) | (Seg n) = odd-seq n by A4, RFUNCT_1:44; :: thesis: verum