theorem :: WALLIS01:7

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