let k be Nat; :: thesis: for L being non empty ZeroStr
for p being sequence of L holds sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))
let L be non empty ZeroStr ; :: thesis: for p being sequence of L holds sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))
let p be sequence of L; :: thesis: sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (sieve (p,(2 * k))) . n = (sieve ((even_part p),(2 * k))) . n
thus (sieve ((even_part p),(2 * k))) . n = (even_part p) . ((2 * k) * n) by Def5
.= p . ((2 * k) * n) by HURWITZ2:def 1
.= (sieve (p,(2 * k))) . n by Def5 ; :: thesis: verum