let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
HT p,T in Upper_Support p,T,i
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
HT p,T in Upper_Support p,T,i
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being non-zero Polynomial of n,L
for i being Element of NAT st 1 <= i & i <= card (Support p) holds
HT p,T in Upper_Support p,T,i
let p be non-zero Polynomial of n,L; :: thesis: for i being Element of NAT st 1 <= i & i <= card (Support p) holds
HT p,T in Upper_Support p,T,i
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= card (Support p) implies HT p,T in Upper_Support p,T,i )
assume A1: ( 1 <= i & i <= card (Support p) ) ; :: thesis: HT p,T in Upper_Support p,T,i
set u = Upper_Support p,T,i;
A2: ( Upper_Support p,T,i c= Support p & card (Upper_Support p,T,i) = i & ( for b, b' being bag of st b in Upper_Support p,T,i & b' in Support p & b <= b',T holds
b' in Upper_Support p,T,i ) ) by A1, Def2;
consider x being Element of Upper_Support p,T,i;
A3: Upper_Support p,T,i <> {} by A1, Def2, CARD_1:47;
then A4: x in Upper_Support p,T,i ;
then reconsider x' = x as Element of Bags n ;
p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then A5: HT p,T in Support p by TERMORD:def 6;
x' <= HT p,T,T by A2, A4, TERMORD:def 6;
hence HT p,T in Upper_Support p,T,i by A1, A3, A5, Def2; :: thesis: verum