let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 n 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 well-unital distributive add-associative right_zeroed associative commutative 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 n st
( b in Support f & HT (p,T) divides b ) )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 n 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 n 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 n st
( b in Support f & HT (p,T) divides b ) )

A1: now :: thesis: ( ex b being bag of n st
( b in Support f & HT (p,T) divides b ) implies f is_reducible_wrt p,T )

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

end;

now :: thesis: ( f is_reducible_wrt p,T implies ex b being bag of n st
( b in Support f & HT (p,T) divides b ) )

assume f is_reducible_wrt p,T ; :: thesis: ex b being bag of n st
( b in Support f & HT (p,T) divides b )
then consider g being Polynomial of n,L such that
A6: f reduces_to g,p,T ;
consider b being bag of n such that
A7: f reduces_to g,p,b,T by A6;
ex s being bag of n st
( s + (HT (p,T)) = b & g = f - (((f . b) / (HC (p,T))) * (s *' p)) ) by A7;
then A8: HT (p,T) divides b by TERMORD:1;
b in Support f by A7;
hence ex b being bag of n st
( b in Support f & HT (p,T) divides b ) by A8; :: thesis: verum

end;

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