theorem Th37: :: WALLIS01:40

for n being non zero Nat holds 'I' . ((2 * n) + 1) = (Product (even-seq n)) / (Product (odd-seq (n + 1)))