let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant )
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being non zero Element of the carrier of (Polynom-Ring F) holds
( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant ) )
assume A: m in card (nonConstantPolys F) ; :: thesis: for p being non zero Element of the carrier of (Polynom-Ring F) holds
( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant )
let p be non zero Element of the carrier of (Polynom-Ring F); :: thesis: ( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant )
set n = card (nonConstantPolys F);

B: now :: thesis: ( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} implies p is constant )

assume B1: Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} ; :: thesis: p is constant

now :: thesis: for b being bag of card (nonConstantPolys F) st b <> EmptyBag (card (nonConstantPolys F)) holds
(Poly (m,p)) . b = 0. F

let b be bag of card (nonConstantPolys F); :: thesis: ( b <> EmptyBag (card (nonConstantPolys F)) implies (Poly (m,p)) . b = 0. F )
assume b <> EmptyBag (card (nonConstantPolys F)) ; :: thesis: (Poly (m,p)) . b = 0. F
then B2: not b in Support (Poly (m,p)) by B1, TARSKI:def 1;
b is Element of Bags (card (nonConstantPolys F)) by PRE_POLY:def 12;
hence (Poly (m,p)) . b = 0. F by B2, POLYNOM1:def 4; :: thesis: verum

end;

then Poly (m,p) is Constant by POLYNOM7:def 7;
then consider a being Element of F such that
C: Poly (m,p) = a | ((card (nonConstantPolys F)),F) by POLYNOM7:17;
p = a | F by C, A, XYZbb;
hence p is constant by RING_4:20; :: thesis: verum

end;

now :: thesis: ( p is constant implies Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} )

assume p is constant ; :: thesis: Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))}
then consider a being Element of F such that
C: p = a | F by RING_4:20;
D: Poly (m,p) = a | ((card (nonConstantPolys F)),F) by C, A, XYZbb;
p <> 0_. F ;
then a | ((card (nonConstantPolys F)),F) <> 0_ ((card (nonConstantPolys F)),F) by A, D, pZero;
hence Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} by D, POLYNOM7:14; :: thesis: verum

end;

hence ( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant ) by B; :: thesis: verum