theorem Th3: :: WALLIS01:6

for n being non zero Nat holds even-seq (n + 1) = (even-seq n) ^ <*(2 * (n + 1))*>