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

proof

thus
Polynom-Ring (n,L) is distributive
:: thesis: verum
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;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

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;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