set e = even_part p;

ex n being Nat st

for i being Nat st i >= n holds

(even_part p) . i = 0. L

ex n being Nat st

for i being Nat st i >= n holds

(even_part p) . i = 0. L

proof

hence
even_part p is finite-Support
; :: thesis: verum
set l = len p;

take len p ; :: thesis: for i being Nat st i >= len p holds

(even_part p) . i = 0. L

(even_part p) . i = 0. L ; :: thesis: verum

end;take len p ; :: thesis: for i being Nat st i >= len p holds

(even_part p) . i = 0. L

now :: thesis: for x being Nat st x >= len p holds

(even_part p) . x = 0. L

hence
for i being Nat st i >= len p holds (even_part p) . x = 0. L

let x be Nat; :: thesis: ( x >= len p implies (even_part p) . x = 0. L )

reconsider i = x as Element of NAT by ORDINAL1:def 12;

assume A1: x >= len p ; :: thesis: (even_part p) . x = 0. L

end;reconsider i = x as Element of NAT by ORDINAL1:def 12;

assume A1: x >= len p ; :: thesis: (even_part p) . x = 0. L

now :: thesis: ( ( i is even & (even_part p) . i = 0. L ) or ( i is odd & (even_part p) . i = 0. L ) )

hence
(even_part p) . x = 0. L
; :: thesis: verumend;

(even_part p) . i = 0. L ; :: thesis: verum