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 11;
reconsider p = p, q = q as Element of (Polynom-Ring (n,L)) ;
A1: (Polynom-Evaluation (n,L,x)) . p = eval (p9,x) by Def3;
(Polynom-Evaluation (n,L,x)) . (p * q) = (Polynom-Evaluation (n,L,x)) . (p9 *' q9) by POLYNOM1:def 11
.= eval ((p9 *' q9),x) by Def3
.= (eval (p9,x)) * (eval (q9,x)) by Th17 ;
hence (Polynom-Evaluation (n,L,x)) . (p * q) = ((Polynom-Evaluation (n,L,x)) . p) * ((Polynom-Evaluation (n,L,x)) . q) by A1, Def3; :: thesis: verum

end;

hence Polynom-Evaluation (n,L,x) is multiplicative by GROUP_6:def 6; :: thesis: verum