let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L
for b, b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty ZeroStr
for p being Polynomial of n,L
for b, b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of n,L
for b, b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T
let p be Polynomial of n,L; :: thesis: for b, b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T
let b, b9 be bag of n; :: thesis: ( b9 in Support (b *' p) implies b9 <= b + (HT (p,T)),T )
assume A1: b9 in Support (b *' p) ; :: thesis: b9 <= b + (HT (p,T)),T
Support (b *' p) c= { (b + b2) where b2 is Element of Bags n : b2 in Support p } by Lm10;
then b9 in { (b + b2) where b2 is Element of Bags n : b2 in Support p } by A1;
then consider s being Element of Bags n such that
A2: b9 = b + s and
A3: s in Support p ;
s <= HT (p,T),T by A3, TERMORD:def 6;
then [s,(HT (p,T))] in T by TERMORD:def 2;
then [(b + s),(b + (HT (p,T)))] in T by BAGORDER:def 5;
hence b9 <= b + (HT (p,T)),T by A2, TERMORD:def 2; :: thesis: verum