set f = Polynom-Evaluation n,L,x;
for p, q being Element of (Polynom-Ring n,L) holds (Polynom-Evaluation n,L,x) . (p + q) = ((Polynom-Evaluation n,L,x) . p) + ((Polynom-Evaluation n,L,x) . q)

proof

let p, q be Element of (Polynom-Ring n,L); :: thesis: (Polynom-Evaluation n,L,x) . (p + q) = ((Polynom-Evaluation n,L,x) . p) + ((Polynom-Evaluation n,L,x) . q)
reconsider p9 = p, q9 = q as Polynomial of n,L by POLYNOM1:def 27;
reconsider p = p, q = q as Element of (Polynom-Ring n,L) ;
A1: (Polynom-Evaluation n,L,x) . p = eval p9,x by Def5;
(Polynom-Evaluation n,L,x) . (p + q) = (Polynom-Evaluation n,L,x) . (p9 + q9) by POLYNOM1:def 27
.= eval (p9 + q9),x by Def5
.= (eval p9,x) + (eval q9,x) by Th25 ;
hence (Polynom-Evaluation n,L,x) . (p + q) = ((Polynom-Evaluation n,L,x) . p) + ((Polynom-Evaluation n,L,x) . q) by A1, Def5; :: thesis: verum

end;

hence Polynom-Evaluation n,L,x is additive by GRCAT_1:def 13; :: thesis: verum