let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being constant Polynomial of F holds
( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being constant Polynomial of F holds
( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 ) )
assume AS: m in card (nonConstantPolys F) ; :: thesis: for p being constant Polynomial of F holds
( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )
let p be constant Polynomial of F; :: thesis: ( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )
set q = Poly (m,p);
set n = card (nonConstantPolys F);
reconsider p1 = p as Element of the carrier of (Polynom-Ring F) by POLYNOM3:def 10;
I: p1 is constant by RATFUNC1:def 2;
field (BagOrder (card (nonConstantPolys F))) = Bags (card (nonConstantPolys F)) by ORDERS_1:12;
then J: BagOrder (card (nonConstantPolys F)) linearly_orders Support (Poly (m,p)) by ORDERS_1:37, ORDERS_1:38;
then B: rng (SgmX ((BagOrder (card (nonConstantPolys F))),(Support (Poly (m,p))))) = Support (Poly (m,p)) by PRE_POLY:def 2;

per cases ( Poly (m,p) <> 0_ ((card (nonConstantPolys F)),F) or Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) ) ;

suppose A: Poly (m,p) <> 0_ ((card (nonConstantPolys F)),F) ; :: thesis: ( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )

consider a being Element of F such that
H: p1 = a | F by I, RING_4:20;
C: Poly (m,p) = a | ((card (nonConstantPolys F)),F) by H, AS, XYZbb;
D: Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))}

proof

E: now :: thesis: for o being object st o in Support (Poly (m,p)) holds
o in {(EmptyBag (card (nonConstantPolys F)))}

let o be object ; :: thesis: ( o in Support (Poly (m,p)) implies o in {(EmptyBag (card (nonConstantPolys F)))} )
assume D2: o in Support (Poly (m,p)) ; :: thesis: o in {(EmptyBag (card (nonConstantPolys F)))}
then reconsider b = o as bag of card (nonConstantPolys F) ;

now :: thesis: not o <> EmptyBag (card (nonConstantPolys F))

assume o <> EmptyBag (card (nonConstantPolys F)) ; :: thesis: contradiction
then D3: support b <> {} by PRE_POLY:81;

per cases ( support b = {m} or support b <> {m} ) ;

suppose D4: support b = {m} ; :: thesis: contradiction

m in {m} by TARSKI:def 1;
then D5: b . m <> 0 by D4, PRE_POLY:def 7;
(Poly (m,p)) . b = p . (b . m) by D4, defPg
.= 0. F by D5, H, Th28 ;
hence contradiction by D2, POLYNOM1:def 4; :: thesis: verum

end;

suppose support b <> {m} ; :: thesis: contradiction

then (Poly (m,p)) . b = 0. F by D3, defPg;
hence contradiction by D2, POLYNOM1:def 4; :: thesis: verum

end;

end;

end;

hence o in {(EmptyBag (card (nonConstantPolys F)))} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for o being object st o in {(EmptyBag (card (nonConstantPolys F)))} holds
o in Support (Poly (m,p))

let o be object ; :: thesis: ( o in {(EmptyBag (card (nonConstantPolys F)))} implies o in Support (Poly (m,p)) )
assume o in {(EmptyBag (card (nonConstantPolys F)))} ; :: thesis: o in Support (Poly (m,p))
then D1: o = EmptyBag (card (nonConstantPolys F)) by TARSKI:def 1;
D2: (Poly (m,p)) . (EmptyBag (card (nonConstantPolys F))) = p . 0 by defPg
.= a by H, Th28 ;
a <> 0. F by A, C, POLYNOM7:19;
hence o in Support (Poly (m,p)) by D1, D2, POLYNOM1:def 4; :: thesis: verum

end;

hence Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} by E, TARSKI:2; :: thesis: verum

end;

then E: card (Support (Poly (m,p))) = 1 by CARD_1:30;
then C: len (SgmX ((BagOrder (card (nonConstantPolys F))),(Support (Poly (m,p))))) = 1 by J, PRE_POLY:11;
SgmX ((BagOrder (card (nonConstantPolys F))),(Support (Poly (m,p)))) = <*(EmptyBag (card (nonConstantPolys F)))*> by D, B, E, J, PRE_POLY:11, FINSEQ_1:39;
hence Lt (Poly (m,p)) = <*(EmptyBag (card (nonConstantPolys F)))*> . 1 by C, A, defLT
.= EmptyBag (card (nonConstantPolys F)) ;
:: thesis: LC (Poly (m,p)) = p . 0
hence LC (Poly (m,p)) = p . 0 by defPg; :: thesis: verum

end;

suppose Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) ; :: thesis: ( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )

hence Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) by defLT; :: thesis: LC (Poly (m,p)) = p . 0
hence LC (Poly (m,p)) = p . 0 by defPg; :: thesis: verum

end;

end;