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:31
.= eval ((1_ (n,L)),x) by Def3
.= 1_ L by Th13 ; :: according to GROUP_1:def 13 :: thesis: verum