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 Th21 ; :: according to GROUP_1:def 17 :: thesis: verum