let n be Ordinal; for T being connected admissible TermOrder of n
for L being non empty non degenerated 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
for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
let T be connected admissible TermOrder of n; for L being non empty non degenerated 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
for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
let L be non empty non degenerated 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
for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
let P be Subset of (Polynom-Ring (n,L)); for f being Polynomial of n,L
for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
let f be Polynomial of n,L; for m being Monomial of n,L st PolyRedRel (P,T) reduces f, 0_ (n,L) holds
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
let m be Monomial of n,L; ( PolyRedRel (P,T) reduces f, 0_ (n,L) implies PolyRedRel (P,T) reduces m *' f, 0_ (n,L) )
assume
PolyRedRel (P,T) reduces f, 0_ (n,L)
; PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
then
PolyRedRel (P,T) reduces m *' f,m *' (0_ (n,L))
by Th47;
hence
PolyRedRel (P,T) reduces m *' f, 0_ (n,L)
by POLYNOM1:28; verum