let p, q be Polynomial of F_Real; :: thesis: Eval (p + q) = (Eval p) + (Eval q)
let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (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 ;
:: thesis: verum