let R be non degenerated comRing; :: thesis: for p0 being Element of (Polynom-Ring (0,R)) holds p0 is not Polynomial of (Polynom-Ring (0,R))
let p0 be Element of (Polynom-Ring (0,R)); :: thesis: p0 is not Polynomial of (Polynom-Ring (0,R))
reconsider P0 = p0 as Series of 0,R by POLYNOM1:def 11;
not p0 in [#] (Polynom-Ring (Polynom-Ring (0,R)))

proof

assume p0 in [#] (Polynom-Ring (Polynom-Ring (0,R))) ; :: thesis: contradiction
then reconsider P1 = p0 as sequence of (Polynom-Ring (0,R)) by POLYNOM3:def 10;
A2: dom P1 = NAT by FUNCT_2:def 1;
1 --> 0 in Bags 1 by PRE_POLY:def 12;
then dom P0 <> dom P1 by A2;
hence contradiction ; :: thesis: verum

end;

hence p0 is not Polynomial of (Polynom-Ring (0,R)) by POLYNOM3:def 10; :: thesis: verum