let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of st
( b in Support f & HT p,T divides b ) )
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of st
( b in Support f & HT p,T divides b ) )
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being Polynomial of n,L
for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of st
( b in Support f & HT p,T divides b ) )
let f be Polynomial of n,L; :: thesis: for p being non-zero Polynomial of n,L holds
( f is_reducible_wrt p,T iff ex b being bag of st
( b in Support f & HT p,T divides b ) )
let p be non-zero Polynomial of n,L; :: thesis: ( f is_reducible_wrt p,T iff ex b being bag of st
( b in Support f & HT p,T divides b ) )

A1: now

assume f is_reducible_wrt p,T ; :: thesis: ex b being bag of st
( b in Support f & HT p,T divides b )
then consider g being Polynomial of n,L such that
A2: f reduces_to g,p,T by Def8;
consider b being bag of such that
A3: f reduces_to g,p,b,T by A2, Def6;
A4: ( 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 A3, Def5;
then HT p,T divides b by TERMORD:1;
hence ex b being bag of st
( b in Support f & HT p,T divides b ) by A4; :: thesis: verum

end;

now

assume ex b being bag of st
( b in Support f & HT p,T divides b ) ; :: thesis: f is_reducible_wrt p,T
then consider b being bag of such that
A5: ( b in Support f & HT p,T divides b ) ;
consider s being bag of such that
A6: b = (HT p,T) + s by A5, TERMORD:1;
set g = f - (((f . b) / (HC p,T)) * (s *' p));
( f <> 0_ n,L & p <> 0_ n,L ) by A5, POLYNOM7:1, POLYNOM7:def 2;
then f reduces_to f - (((f . b) / (HC p,T)) * (s *' p)),p,b,T by A5, A6, Def5;
then f reduces_to f - (((f . b) / (HC p,T)) * (s *' p)),p,T by Def6;
hence f is_reducible_wrt p,T by Def8; :: thesis: verum

end;

hence ( f is_reducible_wrt p,T iff ex b being bag of st
( b in Support f & HT p,T divides b ) ) by A1; :: thesis: verum