set R = Polynom-Ring L;

now :: thesis: for x being Element of (Polynom-Ring L) holds
( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x )

let x be Element of (Polynom-Ring L); :: thesis: ( x * (1. (Polynom-Ring L)) = x & (1. (Polynom-Ring L)) * x = x )
reconsider p = x as Polynomial of L by POLYNOM3:def 10;
set e = 1. (Polynom-Ring L);
A2: 1. (Polynom-Ring L) = 1_. L by POLYNOM3:def 10;
hence x * (1. (Polynom-Ring L)) = p *' (1_. L) by POLYNOM3:def 10
.= x by POLYNOM3:35 ;
:: thesis: (1. (Polynom-Ring L)) * x = x
thus (1. (Polynom-Ring L)) * x = (1_. L) *' p by A2, POLYNOM3:def 10
.= x by poly1 ; :: thesis: verum

end;

hence Polynom-Ring L is well-unital by VECTSP_1:def 6; :: thesis: verum