set Pm = Polynom-Ring n,L;
thus Polynom-Ring n,L is well-unital :: thesis: Polynom-Ring n,L is right-distributive

proof

let x be Element of (Polynom-Ring n,L); :: according to VECTSP_1:def 16 :: thesis: ( x * (1. (Polynom-Ring n,L)) = x & (1. (Polynom-Ring n,L)) * x = x )
thus ( x * (1. (Polynom-Ring n,L)) = x & (1. (Polynom-Ring n,L)) * x = x ) by Lm5; :: thesis: verum

end;

let x, y, z be Element of (Polynom-Ring n,L); :: according to VECTSP_1:def 11 :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider p = x, q = y, r = z as Polynomial of n,L by Def27;
A1: ( x * y = p *' q & x * z = p *' r ) by Def27;
y + z = q + r by Def27;
hence x * (y + z) = p *' (q + r) by Def27
.= (p *' q) + (p *' r) by Th85
.= (x * y) + (x * z) by A1, Def27 ;
:: thesis: verum