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 6 :: 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 Lm1; :: thesis: verum

end;

let x, y, z be Element of (Polynom-Ring (n,L)); :: according to VECTSP_1:def 2 :: 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