let k be Nat; 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 ; for p being sequence of L holds sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))
let p be sequence of L; sieve (p,(2 * k)) = sieve ((even_part p),(2 * k))
let n be Element of NAT ; FUNCT_2:def 8 (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
; verum