let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT p,T <= HT f,T,T
let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT p,T <= HT f,T,T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT p,T <= HT f,T,T
let f, p be non-zero Polynomial of n,L; :: thesis: ( f is_reducible_wrt p,T implies HT p,T <= HT f,T,T )
assume f is_reducible_wrt p,T ; :: thesis: HT p,T <= HT f,T,T
then consider b being bag of such that
A1: ( b in Support f & HT p,T divides b ) by POLYRED:36;
A2: b <= HT f,T,T by A1, TERMORD:def 6;
HT p,T <= b,T by A1, TERMORD:10;
hence HT p,T <= HT f,T,T by A2, TERMORD:8; :: thesis: verum