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))));

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

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)

then
Polynomial-Function (L,(rpoly (1,(0. L)))) is odd
;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;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

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