let n be set ; :: thesis: for L being non empty ZeroStr
for p being Series of n,L holds
( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) )
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L holds
( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) )
let p be Series of n,L; :: thesis: ( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) )

A1: now :: thesis: ( not p is ConstPoly of n,L or Support p = {(EmptyBag n)} or p = 0_ (n,L) )

assume A2: p is ConstPoly of n,L ; :: thesis: ( Support p = {(EmptyBag n)} or p = 0_ (n,L) )
A3: for u being object st u in Support p holds
u in {(EmptyBag n)}

proof

let u be object ; :: thesis: ( u in Support p implies u in {(EmptyBag n)} )
assume A4: u in Support p ; :: thesis: u in {(EmptyBag n)}
then reconsider u = u as Element of Bags n ;
reconsider u9 = u as bag of n ;
p . u9 <> 0. L by A4, POLYNOM1:def 4;
then u9 = EmptyBag n by A2, Def7;
hence u in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum

end;

thus ( Support p = {(EmptyBag n)} or p = 0_ (n,L) ) :: thesis: verum

proof

assume A5: not Support p = {(EmptyBag n)} ; :: thesis: p = 0_ (n,L)
A6: not EmptyBag n in Support p

proof

assume EmptyBag n in Support p ; :: thesis: contradiction
then for u being object st u in {(EmptyBag n)} holds
u in Support p by TARSKI:def 1;
hence contradiction by A3, A5, TARSKI:2; :: thesis: verum

end;

A7: Support p = {}

proof

set v = the Element of Support p;
assume Support p <> {} ; :: thesis: contradiction
then ( the Element of Support p in Support p & the Element of Support p in {(EmptyBag n)} ) by A3;
hence contradiction by A6, TARSKI:def 1; :: thesis: verum

end;

A8: for b being bag of n holds p . b = 0. L

proof

let b be bag of n; :: thesis: p . b = 0. L
A9: b is Element of Bags n by PRE_POLY:def 12;
assume p . b <> 0. L ; :: thesis: contradiction
hence contradiction by A7, A9, POLYNOM1:def 4; :: thesis: verum

end;

A10: for u being object st u in rng p holds
u in {(0. L)}

proof

let u be object ; :: thesis: ( u in rng p implies u in {(0. L)} )
assume u in rng p ; :: thesis: u in {(0. L)}
then consider x being object such that
A11: x in dom p and
A12: p . x = u by FUNCT_1:def 3;
x is bag of n by A11;
then u = 0. L by A8, A12;
hence u in {(0. L)} by TARSKI:def 1; :: thesis: verum

end;

A13: dom p = Bags n by FUNCT_2:def 1;
for u being object st u in {(0. L)} holds
u in rng p

proof

set b = the bag of n;
let u be object ; :: thesis: ( u in {(0. L)} implies u in rng p )
assume u in {(0. L)} ; :: thesis: u in rng p
then u = 0. L by TARSKI:def 1;
then A14: p . the bag of n = u by A8;
the bag of n in dom p by A13, PRE_POLY:def 12;
hence u in rng p by A14, FUNCT_1:def 3; :: thesis: verum

end;

then rng p = {(0. L)} by A10, TARSKI:2;
then p = (Bags n) --> (0. L) by A13, FUNCOP_1:9;
hence p = 0_ (n,L) by POLYNOM1:def 8; :: thesis: verum

end;

end;

now :: thesis: ( ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) implies p is ConstPoly of n,L )

assume A15: ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) ; :: thesis: p is ConstPoly of n,L

per cases ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) by A15;

suppose p = 0_ (n,L) ; :: thesis: p is ConstPoly of n,L

then for b being bag of n st b <> EmptyBag n holds
p . b = 0. L by POLYNOM1:22;
hence p is ConstPoly of n,L by Def7; :: thesis: verum

end;

suppose A16: Support p = {(EmptyBag n)} ; :: thesis: p is ConstPoly of n,L

for b being bag of n st b <> EmptyBag n holds
p . b = 0. L

proof

let b be bag of n; :: thesis: ( b <> EmptyBag n implies p . b = 0. L )
assume A17: b <> EmptyBag n ; :: thesis: p . b = 0. L
reconsider b = b as Element of Bags n by PRE_POLY:def 12;
not b in Support p by A16, A17, TARSKI:def 1;
hence p . b = 0. L by POLYNOM1:def 4; :: thesis: verum

end;

hence p is ConstPoly of n,L by Def7; :: thesis: verum

end;

end;

end;

hence ( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {(EmptyBag n)} ) ) by A1; :: thesis: verum