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