:: deftheorem Def5 defines sieve BASEL_2:def 5 :
for L being non empty set
for p being sequence of L
for m being Nat
for b₄ being sequence of L holds
( b₄ = sieve (p,m) iff for i being Nat holds b₄ . i = p . (m * i) );