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 P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) holds

for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 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 P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) holds

for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) holds

for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) implies for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) )

assume A1: for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ; :: thesis: for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ; :: thesis: verum

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) holds

for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 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 P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) holds

for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) holds

for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( ( for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ) implies for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) )

assume A1: for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_top_reducible_wrt P,T ; :: thesis: for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

now :: thesis: for b being bag of n st b in HT ((P -Ideal),T) holds

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

hence
for b being bag of n st b in HT ((P -Ideal),T) holds ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

let b be bag of n; :: thesis: ( b in HT ((P -Ideal),T) implies ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) )

assume b in HT ((P -Ideal),T) ; :: thesis: ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

then consider p being Polynomial of n,L such that

A2: b = HT (p,T) and

A3: p in P -Ideal and

A4: p <> 0_ (n,L) ;

reconsider p = p as non-zero Polynomial of n,L by A4, POLYNOM7:def 1;

p is_top_reducible_wrt P,T by A1, A3;

then consider u being Polynomial of n,L such that

A5: u in P and

A6: p is_top_reducible_wrt u,T by POLYRED:def 12;

consider q being Polynomial of n,L such that

A7: p top_reduces_to q,u,T by A6, POLYRED:def 11;

A8: p reduces_to q,u, HT (p,T),T by A7, POLYRED:def 10;

then u <> 0_ (n,L) by POLYRED:def 5;

then A9: HT (u,T) in { (HT (r,T)) where r is Polynomial of n,L : ( r in P & r <> 0_ (n,L) ) } by A5;

ex s being bag of n st

( s + (HT (u,T)) = HT (p,T) & q = p - (((p . (HT (p,T))) / (HC (u,T))) * (s *' u)) ) by A8, POLYRED:def 5;

hence ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) by A2, A9, PRE_POLY:50; :: thesis: verum

end;( b9 in HT (P,T) & b9 divides b ) )

assume b in HT ((P -Ideal),T) ; :: thesis: ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b )

then consider p being Polynomial of n,L such that

A2: b = HT (p,T) and

A3: p in P -Ideal and

A4: p <> 0_ (n,L) ;

reconsider p = p as non-zero Polynomial of n,L by A4, POLYNOM7:def 1;

p is_top_reducible_wrt P,T by A1, A3;

then consider u being Polynomial of n,L such that

A5: u in P and

A6: p is_top_reducible_wrt u,T by POLYRED:def 12;

consider q being Polynomial of n,L such that

A7: p top_reduces_to q,u,T by A6, POLYRED:def 11;

A8: p reduces_to q,u, HT (p,T),T by A7, POLYRED:def 10;

then u <> 0_ (n,L) by POLYRED:def 5;

then A9: HT (u,T) in { (HT (r,T)) where r is Polynomial of n,L : ( r in P & r <> 0_ (n,L) ) } by A5;

ex s being bag of n st

( s + (HT (u,T)) = HT (p,T) & q = p - (((p . (HT (p,T))) / (HC (u,T))) * (s *' u)) ) by A8, POLYRED:def 5;

hence ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) by A2, A9, PRE_POLY:50; :: thesis: verum

ex b9 being bag of n st

( b9 in HT (P,T) & b9 divides b ) ; :: thesis: verum