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, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convergent_wrt PolyRedRel (P,T)
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, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convergent_wrt PolyRedRel (P,T)
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, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convergent_wrt PolyRedRel (P,T)
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f, g being Polynomial of n,L st PolyRedRel (P,T) reduces f - g, 0_ (n,L) holds
f,g are_convergent_wrt PolyRedRel (P,T)
let f, g be Polynomial of n,L; :: thesis: ( PolyRedRel (P,T) reduces f - g, 0_ (n,L) implies f,g are_convergent_wrt PolyRedRel (P,T) )
assume PolyRedRel (P,T) reduces f - g, 0_ (n,L) ; :: thesis: f,g are_convergent_wrt PolyRedRel (P,T)
then consider f1, g1 being Polynomial of n,L such that
A1: f1 - g1 = 0_ (n,L) and
A2: ( PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 ) by Th49;
g1 = (f1 - g1) + g1 by A1, Th2
.= (f1 + (- g1)) + g1 by POLYNOM1:def 7
.= f1 + ((- g1) + g1) by POLYNOM1:21
.= f1 + (0_ (n,L)) by Th3
.= f1 by POLYNOM1:23 ;
hence f,g are_convergent_wrt PolyRedRel (P,T) by A2, REWRITE1:def 7; :: thesis: verum