theorem Th12: :: WALLIS01:15

for k being non zero Nat holds Product (odd-seq k) = ((2 * k) !) / ((2 |^ k) * (k !))