theorem Th9: :: WALLIS01:12

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