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 Th27 ;
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 multiplicative by GROUP_6:def 7; :: thesis: verum