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)} ) )

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)}

end;A3: for u being object st u in Support p holds

u in {(EmptyBag n)}

proof

thus
( Support p = {(EmptyBag n)} or p = 0_ (n,L) )
:: thesis: verum
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;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

proof

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

A6: not EmptyBag n in Support p

u in {(0. L)}

for u being object st u in {(0. L)} holds

u in rng p

then p = (Bags n) --> (0. L) by A13, FUNCOP_1:9;

hence p = 0_ (n,L) by POLYNOM1:def 8; :: thesis: verum

end;A6: not EmptyBag n in Support p

proof

A7:
Support p = {}
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;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

proof

A8:
for b being bag of n holds p . b = 0. L
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;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

proof

A10:
for u being object st u in rng p holds
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;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

u in {(0. L)}

proof

A13:
dom p = Bags n
by FUNCT_2:def 1;
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;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

for u being object st u in {(0. L)} holds

u in rng p

proof

then
rng p = {(0. L)}
by A10, TARSKI:2;
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;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

then p = (Bags n) --> (0. L) by A13, FUNCOP_1:9;

hence p = 0_ (n,L) by POLYNOM1:def 8; :: thesis: verum

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

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

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

end;

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;p . b = 0. L by POLYNOM1:22;

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

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

end;p . b = 0. L

proof

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