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

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

proof

let u be set ; :: 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 u' = u as bag of n ;
p . u' <> 0. L by A4, POLYNOM1:def 9;
then u' = EmptyBag n by A2, Def8;
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 set 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

assume A8: Support p <> {} ; :: thesis: contradiction
consider v being Element of Support p;
A9: v in Support p by A8;
v in {(EmptyBag n)} by A3, A8;
hence contradiction by A6, A9, TARSKI:def 1; :: thesis: verum

end;

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

proof

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

end;

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

proof

let u be set ; :: thesis: ( u in rng p implies u in {(0. L)} )
assume u in rng p ; :: thesis: u in {(0. L)}
then consider x being set such that
A14: ( x in dom p & p . x = u ) by FUNCT_1:def 5;
x is bag of n by A14, POLYNOM1:def 14;
then u = 0. L by A10, A14;
hence u in {(0. L)} by TARSKI:def 1; :: thesis: verum

end;

for u being set st u in {(0. L)} holds
u in rng p

proof

let u be set ; :: thesis: ( u in {(0. L)} implies u in rng p )
assume u in {(0. L)} ; :: thesis: u in rng p
then A15: u = 0. L by TARSKI:def 1;
consider b being bag of n;
A16: p . b = u by A10, A15;
b in dom p by A12, POLYNOM1:def 14;
hence u in rng p by A16, FUNCT_1:def 5; :: thesis: verum

end;

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

end;

end;

now

assume A17: ( 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 A17;

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:81;
hence p is ConstPoly of n,L by Def8; :: thesis: verum

end;

suppose A18: 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 A19: b <> EmptyBag n ; :: thesis: p . b = 0. L
reconsider b = b as Element of Bags n by POLYNOM1:def 14;
not b in Support p by A18, A19, TARSKI:def 1;
hence p . b = 0. L by POLYNOM1:def 9; :: thesis: verum

end;

hence p is ConstPoly of n,L by Def8; :: 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