theorem Th22: :: BASEL_2:22

for L being Field
for p being Polynomial of L holds even_part p = Subst ((sieve (p,2)),<%(0. L),(0. L),(1_ L)%>)