theorem Th1: :: WALLIS01:4

for n being non zero Nat holds
( dom (even-seq n) = Seg n & dom (odd-seq n) = Seg n & len (odd-seq n) = n & len (even-seq n) = n )