thus (Polynom-Evaluation (L,x)) . (1_ (Polynom-Ring L)) = (Polynom-Evaluation (L,x)) . (1_. L) by POLYNOM3:36
.= eval ((1_. L),x) by Def3
.= 1_ L by Th21 ; :: according to GROUP_1:def 13 :: thesis: verum