set p = rpoly (1,(0. L));
take rpoly (1,(0. L)) ; :: thesis: ( not rpoly (1,(0. L)) is zero & rpoly (1,(0. L)) is odd )
set f = Polynomial-Function (L,(rpoly (1,(0. L))));

now :: thesis: for x being Element of L holds (Polynomial-Function (L,(rpoly (1,(0. L))))) . (- x) = - ((Polynomial-Function (L,(rpoly (1,(0. L))))) . x)

let x be Element of L; :: thesis: (Polynomial-Function (L,(rpoly (1,(0. L))))) . (- x) = - ((Polynomial-Function (L,(rpoly (1,(0. L))))) . x)
thus (Polynomial-Function (L,(rpoly (1,(0. L))))) . (- x) = eval ((rpoly (1,(0. L))),(- x)) by POLYNOM5:def 13
.= (- x) - (0. L) by HURWITZ:29
.= - x by RLVECT_1:13
.= - (x - (0. L)) by RLVECT_1:13
.= - (eval ((rpoly (1,(0. L))),x)) by HURWITZ:29
.= - ((Polynomial-Function (L,(rpoly (1,(0. L))))) . x) by POLYNOM5:def 13 ; :: thesis: verum

end;

then Polynomial-Function (L,(rpoly (1,(0. L)))) is odd ;
hence ( not rpoly (1,(0. L)) is zero & rpoly (1,(0. L)) is odd ) ; :: thesis: verum