let p, q be Polynomial of F_Real; Eval (p + q) = (Eval p) + (Eval q)
let r be Element of REAL ; FUNCT_2:def 8 (Eval (p + q)) . r = ((Eval p) + (Eval q)) . r
set s = In (r,F_Real);
( (Eval p) . r = eval (p,(In (r,F_Real))) & (Eval q) . r = eval (q,(In (r,F_Real))) )
by POLYNOM5:def 13;
hence ((Eval p) + (Eval q)) . r =
(eval (p,(In (r,F_Real)))) + (eval (q,(In (r,F_Real))))
by VALUED_1:1
.=
eval ((p + q),(In (r,F_Real)))
by POLYNOM4:19
.=
(Eval (p + q)) . r
by POLYNOM5:def 13
;
verum