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 p' = p, q' = 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 + q) = (Polynom-Evaluation n,L,x) . (p' + q') by POLYNOM1:def 27
.= eval (p' + q'),x by Def5
.= (eval p',x) + (eval q',x) by Th25 ;
( (Polynom-Evaluation n,L,x) . p = eval p',x & (Polynom-Evaluation n,L,x) . q = eval q',x ) by Def5;
hence (Polynom-Evaluation n,L,x) . (p + q) = ((Polynom-Evaluation n,L,x) . p) + ((Polynom-Evaluation n,L,x) . q) by A1; :: thesis: verum

end;

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