let a, b be Element of (Polynom-Ring L); :: according to GROUP_6:def 6 :: thesis: (Polynom-Evaluation (L,x)) . (a * b) = ((Polynom-Evaluation (L,x)) . a) * ((Polynom-Evaluation (L,x)) . b)
reconsider p = a, q = b as Polynomial of L by POLYNOM3:def 10;
thus (Polynom-Evaluation (L,x)) . (a * b) = (Polynom-Evaluation (L,x)) . (p *' q) by POLYNOM3:def 10
.= eval ((p *' q),x) by Def3
.= (eval (p,x)) * (eval (q,x)) by Th24
.= ((Polynom-Evaluation (L,x)) . a) * (eval (q,x)) by Def3
.= ((Polynom-Evaluation (L,x)) . a) * ((Polynom-Evaluation (L,x)) . b) by Def3 ; :: thesis: verum