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 Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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