:: deftheorem Def7 defines Wallis_Seq WALLIS01:def 6 :
for b₁ being Real_Sequence holds
( b₁ = Wallis_Seq iff for k being Nat holds b₁ . k = (((Product (odd-seq (k + 1))) |^ 2) / ((Product (even-seq (k + 1))) |^ 2)) * (k + 1) );