let a, b be Element of (Polynom-Ring L); :: according to GROUP_6:def 7 :: 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 12;
thus (Polynom-Evaluation L,x) . (a * b) = (Polynom-Evaluation L,x) . (p *' q) by POLYNOM3:def 12
.= eval (p *' q),x by Def3
.= (eval p,x) * (eval q,x) by Th27
.= ((Polynom-Evaluation L,x) . a) * (eval q,x) by Def3
.= ((Polynom-Evaluation L,x) . a) * ((Polynom-Evaluation L,x) . b) by Def3 ; :: thesis: verum