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 = {()} ) )

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 = {()} ) )

let p be Series of n,L; :: thesis: ( p is ConstPoly of n,L iff ( p = 0_ (n,L) or Support p = {()} ) )
A1: now :: thesis: ( not p is ConstPoly of n,L or Support p = {()} or p = 0_ (n,L) )
assume A2: p is ConstPoly of n,L ; :: thesis: ( Support p = {()} or p = 0_ (n,L) )
A3: for u being object st u in Support p holds
u in {()}
proof
let u be object ; :: thesis: ( u in Support p implies u in {()} )
assume A4: u in Support p ; :: thesis: u in {()}
then reconsider u = u as Element of Bags n ;
reconsider u9 = u as bag of n ;
p . u9 <> 0. L by ;
then u9 = EmptyBag n by ;
hence u in {()} by TARSKI:def 1; :: thesis: verum
end;
thus ( Support p = {()} or p = 0_ (n,L) ) :: thesis: verum
proof
assume A5: not Support p = {()} ; :: thesis: p = 0_ (n,L)
A6: not EmptyBag n in Support p 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 {()} ) 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 ;
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 ;
hence u in rng p by ; :: thesis: verum
end;
then rng p = {(0. L)} by ;
then p = (Bags n) --> (0. L) by ;
hence p = 0_ (n,L) by POLYNOM1:def 8; :: thesis: verum
end;
end;
now :: thesis: ( ( p = 0_ (n,L) or Support p = {()} ) implies p is ConstPoly of n,L )
assume A15: ( p = 0_ (n,L) or Support p = {()} ) ; :: thesis: p is ConstPoly of n,L
per cases ( p = 0_ (n,L) or Support p = {()} ) 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 = {()} ; :: 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 ;
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 = {()} ) ) by A1; :: thesis: verum