set f = Polynom-Evaluation n,L,x;
for p, q being Element of 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 ; :: 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 ;
A1: (Polynom-Evaluation n,L,x) . p = eval p',x by Def5;
(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 ;
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