set e = even_part p;
ex n being Nat st
for i being Nat st i >= n holds
(even_part p) . i = 0. L

proof

set l = len p;
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

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

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

per cases ( i is even or i is odd ) ;

case i is even ; :: thesis: (even_part p) . i = 0. L

hence (even_part p) . i = p . i by Def1
.= 0. L by A1, ALGSEQ_1:8 ;
:: thesis: verum

end;

case i is odd ; :: thesis: (even_part p) . i = 0. L

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

end;

end;

end;

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

end;

hence for i being Nat st i >= len p holds
(even_part p) . i = 0. L ; :: thesis: verum

end;

hence even_part p is finite-Support ; :: thesis: verum