theorem Th5: :: WALLIS01:8

( even-seq 1 = <*2*> & even-seq 2 = <*2,4*> & even-seq 3 = <*2,4,6*> )