:: deftheorem Def6 defines 'I' WALLIS01:def 5 :
for b₁ being Real_Sequence holds
( b₁ = 'I' iff for m being Nat holds b₁ . m = integral ((@ ((@ sin) |^ m)),0,(PI / 2)) );