let n be non zero Nat; :: thesis: ( dom (even-seq n) = Seg n & dom (odd-seq n) = Seg n & len (odd-seq n) = n & len (even-seq n) = n )
A1: dom (even-seq n) = Seg (len (even-seq n)) by FINSEQ_1:def 3
.= Seg n by Def1 ;
set h = (even-seq n) + ((dom (even-seq n)) --> (- 1));
dom ((even-seq n) + ((dom (even-seq n)) --> (- 1))) = (dom (even-seq n)) /\ (dom ((dom (even-seq n)) --> (- 1))) by VALUED_1:def 1
.= dom (even-seq n) ;
then A2: dom ((even-seq n) + ((dom (even-seq n)) --> (- 1))) = Seg (len (even-seq n)) by FINSEQ_1:def 3
.= Seg n by Def1 ;
len (odd-seq n) = len (even-seq n) by A1, A2, FINSEQ_3:29
.= n by Def1 ;
hence ( dom (even-seq n) = Seg n & dom (odd-seq n) = Seg n & len (odd-seq n) = n & len (even-seq n) = n ) by Def1, A1, A2; :: thesis: verum