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 1 <= i & i <= card (Support p) holds
HT p,T in Support (Up p,T,i)
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 1 <= i & i <= card (Support p) holds
HT p,T in Support (Up p,T,i)
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 1 <= i & i <= card (Support p) holds
HT p,T in Support (Up p,T,i)
let p be Polynomial of n,L; :: thesis: for i being Element of NAT st 1 <= i & i <= card (Support p) holds
HT p,T in Support (Up p,T,i)
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= card (Support p) implies HT p,T in Support (Up p,T,i) )
assume A1: ( 1 <= i & i <= card (Support p) ) ; :: thesis: HT p,T in Support (Up p,T,i)
set u = Up p,T,i;
A2: Support (Up p,T,i) = Upper_Support p,T,i by A1, Lm3;
then A3: card (Support (Up p,T,i)) <> 0 by A1, Def2;
consider x being Element of Support (Up p,T,i);
A4: Support (Up p,T,i) <> {} by A3;
then A5: x in Support (Up p,T,i) ;
then reconsider x = x as Element of Bags n ;
A6: Support (Up p,T,i) c= Support p by A1, A2, Def2;
Support p <> {} by A1;
then A7: HT p,T in Support p by TERMORD:def 6;
x <= HT p,T,T by A5, A6, TERMORD:def 6;
hence HT p,T in Support (Up p,T,i) by A1, A2, A4, A7, Def2; :: thesis: verum