let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b' being bag of st b < b',T & f reduces_to g,p,b,T holds
( b' in Support g iff b' in Support f )
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for f, p, g being Polynomial of n,L
for b, b' being bag of st b < b',T & f reduces_to g,p,b,T holds
( b' in Support g iff b' in Support f )
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f, p, g being Polynomial of n,L
for b, b' being bag of st b < b',T & f reduces_to g,p,b,T holds
( b' in Support g iff b' in Support f )
let f, p, g be Polynomial of n,L; :: thesis: for b, b' being bag of st b < b',T & f reduces_to g,p,b,T holds
( b' in Support g iff b' in Support f )
let b, b' be bag of ; :: thesis: ( b < b',T & f reduces_to g,p,b,T implies ( b' in Support g iff b' in Support f ) )
assume A1: b < b',T ; :: thesis: ( not f reduces_to g,p,b,T or ( b' in Support g iff b' in Support f ) )
assume f reduces_to g,p,b,T ; :: thesis: ( b' in Support g iff b' in Support f )
then consider s being bag of such that
A2: ( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) by Def5;
A3: b' is Element of Bags n by POLYNOM1:def 14;

A4: now

assume b' in Support (s *' p) ; :: thesis: contradiction
then A5: b' <= b,T by A2, Th16;
b <= b',T by A1, TERMORD:def 3;
then b = b' by A5, TERMORD:7;
hence contradiction by A1, TERMORD:def 3; :: thesis: verum

end;

A6: now

assume A7: b' in Support g ; :: thesis: b' in Support f
A8: (((f . b) / (HC p,T)) * (s *' p)) . b' = ((f . b) / (HC p,T)) * ((s *' p) . b') by POLYNOM7:def 10
.= ((f . b) / (HC p,T)) * (0. L) by A3, A4, POLYNOM1:def 9
.= 0. L by VECTSP_1:39 ;
(f - (((f . b) / (HC p,T)) * (s *' p))) . b' = (f + (- (((f . b) / (HC p,T)) * (s *' p)))) . b' by POLYNOM1:def 23
.= (f . b') + ((- (((f . b) / (HC p,T)) * (s *' p))) . b') by POLYNOM1:def 21
.= (f . b') + (- (0. L)) by A8, POLYNOM1:def 22
.= (f . b') + (0. L) by RLVECT_1:25
.= f . b' by RLVECT_1:def 7 ;
then f . b' <> 0. L by A2, A7, POLYNOM1:def 9;
hence b' in Support f by A3, POLYNOM1:def 9; :: thesis: verum

end;

now

assume A9: b' in Support f ; :: thesis: b' in Support g
A10: (((f . b) / (HC p,T)) * (s *' p)) . b' = ((f . b) / (HC p,T)) * ((s *' p) . b') by POLYNOM7:def 10
.= ((f . b) / (HC p,T)) * (0. L) by A3, A4, POLYNOM1:def 9
.= 0. L by VECTSP_1:39 ;
(f - (((f . b) / (HC p,T)) * (s *' p))) . b' = (f + (- (((f . b) / (HC p,T)) * (s *' p)))) . b' by POLYNOM1:def 23
.= (f . b') + ((- (((f . b) / (HC p,T)) * (s *' p))) . b') by POLYNOM1:def 21
.= (f . b') + (- (0. L)) by A10, POLYNOM1:def 22
.= (f . b') + (0. L) by RLVECT_1:25
.= f . b' by RLVECT_1:def 7 ;
then g . b' <> 0. L by A2, A9, POLYNOM1:def 9;
hence b' in Support g by A3, POLYNOM1:def 9; :: thesis: verum

end;

hence ( b' in Support g iff b' in Support f ) by A6; :: thesis: verum