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

proof

take 1_ (Polynom-Ring (n,L)) ; :: according to STRUCT_0:def 18 :: thesis: not 1_ (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L))
A1: ( 1_ (Polynom-Ring (n,L)) = 1_ (n,L) & (0_ (n,L)) . (EmptyBag n) = 0. L ) by POLYNOM1:22, POLYNOM1:31;
( 0. L <> 1_ L & 0. (Polynom-Ring (n,L)) = 0_ (n,L) ) by POLYNOM1:def 11;
hence not 1_ (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L)) by A1, POLYNOM1:25; :: 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 7 :: 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 11;
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 11;
y9 + z9 = v + w by POLYNOM1:def 11;
hence x * (y + z) = u *' (v + w) by POLYNOM1:def 11
.= (u *' v) + (u *' w) by POLYNOM1:26
.= (x * y) + (x * z) by A2, POLYNOM1:def 11 ;
:: thesis: (y + z) * x = (y * x) + (z * x)
A3: ( v *' u = y9 * x9 & w *' u = z9 * x9 ) by POLYNOM1:def 11;
y9 + z9 = v + w by POLYNOM1:def 11;
hence (y + z) * x = (v + w) *' u by POLYNOM1:def 11
.= (v *' u) + (w *' u) by Th8
.= (y * x) + (z * x) by A3, POLYNOM1:def 11 ;
:: thesis: verum

end;