set f = Polynom-Evaluation n,L,x;
thus (Polynom-Evaluation n,L,x) . (1_ (Polynom-Ring n,L)) = (Polynom-Evaluation n,L,x) . (1_ n,L) by POLYNOM1:90
.= eval (1_ n,L),x by Def5
.= 1_ L by Th23 ; :: according to GROUP_1:def 17 :: thesis: verum