let p be Polynomial of F_Real; :: thesis: Eval (- p) = - (Eval p)
let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (Eval (- p)) . r = (- (Eval p)) . r
set s = In (r,F_Real);
(Eval p) . r = eval (p,(In (r,F_Real))) by POLYNOM5:def 13;
hence (- (Eval p)) . r = - (eval (p,(In (r,F_Real)))) by VALUED_1:8
.= eval ((- p),(In (r,F_Real))) by POLYNOM4:20
.= (Eval (- p)) . r by POLYNOM5:def 13 ;
:: thesis: verum