theorem Th38: :: WALLIS01:41

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