let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R holds
( LC p = 0. R iff p = 0_ (n,R) )
let n be Ordinal; :: thesis: for p being Polynomial of n,R holds
( LC p = 0. R iff p = 0_ (n,R) )
let p be Polynomial of n,R; :: thesis: ( LC p = 0. R iff p = 0_ (n,R) )
H: Lt p is Element of Bags n by PRE_POLY:def 12;

A: now :: thesis: ( p = 0_ (n,R) implies LC p = 0. R )

assume p = 0_ (n,R) ; :: thesis: LC p = 0. R
then Support p = {} by YY;
hence LC p = 0. R by H, POLYNOM1:def 4; :: thesis: verum

end;

now :: thesis: ( LC p = 0. R implies p = 0_ (n,R) )

assume LC p = 0. R ; :: thesis: p = 0_ (n,R)
then B: not Lt p in Support p by POLYNOM1:def 4;
field (BagOrder n) = Bags n by ORDERS_1:12;
then K: BagOrder n linearly_orders Support p by ORDERS_1:37, ORDERS_1:38;

now :: thesis: not p <> 0_ (n,R)

assume I: p <> 0_ (n,R) ; :: thesis: contradiction
then G: Lt p = (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) by defLT;
L: rng (SgmX ((BagOrder n),(Support p))) = Support p by K, PRE_POLY:def 2;
Support p <> {} by I, YY;
then M: 1 <= len (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:20;
dom (SgmX ((BagOrder n),(Support p))) = Seg (len (SgmX ((BagOrder n),(Support p)))) by FINSEQ_1:def 3;
then len (SgmX ((BagOrder n),(Support p))) in dom (SgmX ((BagOrder n),(Support p))) by M;
hence contradiction by B, L, G, FUNCT_1:def 3; :: thesis: verum

end;

hence p = 0_ (n,R) ; :: thesis: verum

end;

hence ( LC p = 0. R iff p = 0_ (n,R) ) by A; :: thesis: verum