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