let n be Ordinal; for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
f . b9 = g . b9
let T be connected admissible TermOrder of n; for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
f . b9 = g . b9
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; for f, p, g being Polynomial of n,L
for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
f . b9 = g . b9
let f, p, g be Polynomial of n,L; for b, b9 being bag of n st b < b9,T & f reduces_to g,p,b,T holds
f . b9 = g . b9
let b, b9 be bag of n; ( b < b9,T & f reduces_to g,p,b,T implies f . b9 = g . b9 )
assume A1:
b < b9,T
; ( not f reduces_to g,p,b,T or f . b9 = g . b9 )
assume
f reduces_to g,p,b,T
; f . b9 = g . b9
then consider s being bag of n such that
A2:
s + (HT (p,T)) = b
and
A3:
g = f - (((f . b) / (HC (p,T))) * (s *' p))
;
A6:
b9 is Element of Bags n
by PRE_POLY:def 12;
A7: (((f . b) / (HC (p,T))) * (s *' p)) . b9 =
((f . b) / (HC (p,T))) * ((s *' p) . b9)
by POLYNOM7:def 9
.=
((f . b) / (HC (p,T))) * (0. L)
by A6, A4, POLYNOM1:def 4
.=
0. L
;
(f - (((f . b) / (HC (p,T))) * (s *' p))) . b9 =
(f + (- (((f . b) / (HC (p,T))) * (s *' p)))) . b9
by POLYNOM1:def 7
.=
(f . b9) + ((- (((f . b) / (HC (p,T))) * (s *' p))) . b9)
by POLYNOM1:15
.=
(f . b9) + (- (0. L))
by A7, POLYNOM1:17
.=
(f . b9) + (0. L)
by RLVECT_1:12
.=
f . b9
by RLVECT_1:def 4
;
hence
f . b9 = g . b9
by A3; verum