set Pm = Polynom-Ring (n,L);
thus Polynom-Ring (n,L) is well-unital by Lm1; :: thesis: Polynom-Ring (n,L) is right-distributive
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 Def11;
A1: ( x * y = p *' q & x * z = p *' r ) by Def11;
y + z = q + r by Def11;
hence x * (y + z) = p *' (q + r) by Def11
.= (p *' q) + (p *' r) by Th26
.= (x * y) + (x * z) by A1, Def11 ;
:: thesis: verum