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