set P = Polynom-Ring (n,L);

now :: thesis: not 1. (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L))

assume 1. (Polynom-Ring (n,L)) = 0. (Polynom-Ring (n,L)) ; :: thesis: contradiction
then 1_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11
.= 0_ (n,L) by POLYNOM1:def 11 ;
then 1. L = (0_ (n,L)) . (EmptyBag n) by POLYNOM1:25
.= 0. L by POLYNOM1:22 ;
hence contradiction ; :: thesis: verum

end;

hence not Polynom-Ring (n,L) is degenerated ; :: thesis: verum