A1: 1 <= m by NAT_1:14;
consider n being Nat such that
A2: for k being Nat st k >= n holds
p . k = 0. L by ALGSEQ_1:def 1;
take n ; :: according to ALGSEQ_1:def 1 :: thesis: for b₁ being set holds
( not n <= b₁ or (sieve (p,m)) . b₁ = 0. L )
let k be Nat; :: thesis: ( not n <= k or (sieve (p,m)) . k = 0. L )
assume k >= n ; :: thesis: (sieve (p,m)) . k = 0. L
then A3: m * k >= 1 * n by A1, XREAL_1:66;
thus (sieve (p,m)) . k = p . (m * k) by Def5
.= 0. L by A2, A3 ; :: thesis: verum