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, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of st b in Support g holds
b <= 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, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of st b in Support g holds
b <= 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, g being Polynomial of n,L st f reduces_to g,p,T holds
for b being bag of st b in Support g holds
b <= HT f,T,T
let f, p, g be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies for b being bag of st b in Support g holds
b <= HT f,T,T )
assume f reduces_to g,p,T ; :: thesis: for b being bag of st b in Support g holds
b <= HT f,T,T
then consider b being bag of such that
A1: f reduces_to g,p,b,T by Def6;
( b in Support f & ex s being bag of st
( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) ) by A1, Def5;
then A2: b <= HT f,T,T by TERMORD:def 6;
A3: T is_connected_in field T by RELAT_2:def 14;

now

let u be bag of ; :: thesis: ( u in Support g implies u <= HT f,T,T )
assume A4: u in Support g ; :: thesis: u <= HT f,T,T

now

per cases ( u = b or u <> b ) ;

case u = b ; :: thesis: contradiction

hence contradiction by A1, A4, Lm17; :: thesis: verum

end;

case A5: u <> b ; :: thesis: u <= HT f,T,T

( u <= u,T & b <= b,T ) by TERMORD:6;
then ( [u,u] in T & [b,b] in T ) by TERMORD:def 2;
then ( u in field T & b in field T ) by RELAT_1:30;
then A6: ( [u,b] in T or [b,u] in T ) by A3, A5, RELAT_2:def 6;

now

per cases ( u <= b,T or b <= u,T ) by A6, TERMORD:def 2;

case u <= b,T ; :: thesis: u <= HT f,T,T

hence u <= HT f,T,T by A2, TERMORD:8; :: thesis: verum

end;

case b <= u,T ; :: thesis: u <= HT f,T,T

then b < u,T by A5, TERMORD:def 3;
then ( u in Support f iff u in Support g ) by A1, Th40;
hence u <= HT f,T,T by A4, TERMORD:def 6; :: thesis: verum

end;

end;

end;

hence u <= HT f,T,T ; :: thesis: verum

end;

end;

end;

hence u <= HT f,T,T ; :: thesis: verum

end;

hence for b being bag of st b in Support g holds
b <= HT f,T,T ; :: thesis: verum