theorem Th10: :: WALLIS01:13

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