theorem Th19: :: BASEL_2:19

for k being Nat
for L being non empty ZeroStr
for p being sequence of L holds sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))