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

proof

set l = len p;
take len p ; :: thesis: for i being Nat st i >= len p holds
(odd_part p) . i = 0. L

now :: thesis: for x being Nat st x >= len p holds
(odd_part p) . x = 0. L

let x be Nat; :: thesis: ( x >= len p implies (odd_part p) . x = 0. L )
reconsider i = x as Element of NAT by ORDINAL1:def 12;
assume A2: x >= len p ; :: thesis: (odd_part p) . x = 0. L

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

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

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

hence (odd_part p) . i = p . i by Def2
.= 0. L by A2, ALGSEQ_1:8 ;
:: thesis: verum

end;

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

hence (odd_part p) . i = 0. L by Def2; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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