theorem Th11: :: WALLIS01:14

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