thus not Polynom-Ring n,L is trivial :: thesis: Polynom-Ring n,L is distributive

proof

take u = 1_ (Polynom-Ring n,L); :: according to STRUCT_0:def 19 :: thesis: not u = 0. (Polynom-Ring n,L)
A1: ( 1_ (Polynom-Ring n,L) = 1_ n,L & (0_ n,L) . (EmptyBag n) = 0. L ) by POLYNOM1:81, POLYNOM1:90;
( 0. L <> 1_ L & 0. (Polynom-Ring n,L) = 0_ n,L ) by POLYNOM1:def 27;
hence not u = 0. (Polynom-Ring n,L) by A1, POLYNOM1:84; :: thesis: verum

end;

thus Polynom-Ring n,L is distributive :: thesis: verum

proof

let x, y, z be Element of (Polynom-Ring n,L); :: according to VECTSP_1:def 18 :: thesis: ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) )
reconsider u = x, v = y, w = z as Polynomial of n,L by POLYNOM1:def 27;
reconsider x9 = x, y9 = y, z9 = z as Element of (Polynom-Ring n,L) ;
A2: ( u *' v = x9 * y9 & u *' w = x9 * z9 ) by POLYNOM1:def 27;
y9 + z9 = v + w by POLYNOM1:def 27;
hence x * (y + z) = u *' (v + w) by POLYNOM1:def 27
.= (u *' v) + (u *' w) by POLYNOM1:85
.= (x * y) + (x * z) by A2, POLYNOM1:def 27 ;
:: thesis: (y + z) * x = (y * x) + (z * x)
A3: ( v *' u = y9 * x9 & w *' u = z9 * x9 ) by POLYNOM1:def 27;
y9 + z9 = v + w by POLYNOM1:def 27;
hence (y + z) * x = (v + w) *' u by POLYNOM1:def 27
.= (v *' u) + (w *' u) by Th8
.= (y * x) + (z * x) by A3, POLYNOM1:def 27 ;
:: thesis: verum

end;