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 Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds

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

f is_reducible_wrt P,T

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 Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds

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

f is_reducible_wrt P,T

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 Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds

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

f is_reducible_wrt P,T

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

PolyRedRel (P,T) reduces f, 0_ (n,L) ) implies for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_reducible_wrt P,T )

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

PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_reducible_wrt P,T

f is_reducible_wrt P,T ; :: 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 Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds

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

f is_reducible_wrt P,T

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 Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds

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

f is_reducible_wrt P,T

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 Polynomial of n,L st f in P -Ideal holds

PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds

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

f is_reducible_wrt P,T

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

PolyRedRel (P,T) reduces f, 0_ (n,L) ) implies for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_reducible_wrt P,T )

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

PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: for f being non-zero Polynomial of n,L st f in P -Ideal holds

f is_reducible_wrt P,T

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

f is_reducible_wrt P,T

hence
for f being non-zero Polynomial of n,L st f in P -Ideal holds f is_reducible_wrt P,T

let f be non-zero Polynomial of n,L; :: thesis: ( f in P -Ideal implies f is_reducible_wrt P,T )

assume f in P -Ideal ; :: thesis: f is_reducible_wrt P,T

then A2: PolyRedRel (P,T) reduces f, 0_ (n,L) by A1;

f <> 0_ (n,L) by POLYNOM7:def 1;

then ex g being Polynomial of n,L st

( f reduces_to g,P,T & PolyRedRel (P,T) reduces g, 0_ (n,L) ) by A2, Lm5;

hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

end;assume f in P -Ideal ; :: thesis: f is_reducible_wrt P,T

then A2: PolyRedRel (P,T) reduces f, 0_ (n,L) by A1;

f <> 0_ (n,L) by POLYNOM7:def 1;

then ex g being Polynomial of n,L st

( f reduces_to g,P,T & PolyRedRel (P,T) reduces g, 0_ (n,L) ) by A2, Lm5;

hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

f is_reducible_wrt P,T ; :: thesis: verum