let n be Ordinal; for T being connected TermOrder of n
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )
let T be connected TermOrder of n; for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; for p being Polynomial of n,L
for i being Element of NAT st i <= card (Support p) holds
for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )
let p be Polynomial of n,L; for i being Element of NAT st i <= card (Support p) holds
for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )
let i be Element of NAT ; ( i <= card (Support p) implies for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L ) )
set l = Lower_Support (p,T,i);
assume A1:
i <= card (Support p)
; for b being bag of n st b in Support (Low (p,T,i)) holds
( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )
then A2:
(Lower_Support (p,T,i)) /\ (Upper_Support (p,T,i)) = {}
by Th19;
let b be bag of n; ( b in Support (Low (p,T,i)) implies ( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L ) )
assume A3:
b in Support (Low (p,T,i))
; ( (Low (p,T,i)) . b = p . b & (Up (p,T,i)) . b = 0. L )
hence
(Low (p,T,i)) . b = p . b
by Th16; (Up (p,T,i)) . b = 0. L
b in Lower_Support (p,T,i)
by A1, A3, Lm3;
then
not b in Upper_Support (p,T,i)
by A2, XBOOLE_0:def 4;
then A4:
not b in Support (Up (p,T,i))
by A1, Lm3;
b is Element of Bags n
by PRE_POLY:def 12;
hence
(Up (p,T,i)) . b = 0. L
by A4, POLYNOM1:def 4; verum