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 Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f in P -Ideal
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f in P -Ideal
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L))
for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f in P -Ideal
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f being Polynomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
f in P -Ideal
let f be Polynomial of n,L; :: thesis: ( PolyRedRel (P,T) reduces f, 0_ (n,L) implies f in P -Ideal )
assume PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: f in P -Ideal
then f - (0_ (n,L)) in P -Ideal by Th59;
hence f in P -Ideal by Th4; :: thesis: verum