let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated 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
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; :: thesis: for L being non empty non degenerated 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
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 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
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); :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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:87; :: thesis: verum