let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let T be connected TermOrder of n; :: thesis: for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f, g being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let f, g be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring n,L)
for A, B being LeftLinearCombination of P
for b being bag of
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let P be non empty Subset of (Polynom-Ring n,L); :: thesis: for A, B being LeftLinearCombination of P
for b being bag of
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let A, B be LeftLinearCombination of P; :: thesis: for b being bag of
for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let b be bag of ; :: thesis: for i being Element of NAT st A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) holds
B is_Standard_Representation_of f - g,P,b,T
let i be Element of NAT ; :: thesis: ( A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) implies B is_Standard_Representation_of f - g,P,b,T )
assume A1: ( A is_Standard_Representation_of f,P,b,T & B = A | i & g = Sum (A /^ i) ) ; :: thesis: B is_Standard_Representation_of f - g,P,b,T
then A2: ( Sum A = f & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT (m *' p),T <= b,T ) ) ) by Def7;
A = B ^ (A /^ i) by A1, RFINSEQ:21;
then Sum A = (Sum B) + (Sum (A /^ i)) by RLVECT_1:58;
then (Sum A) + (- (Sum (A /^ i))) = (Sum B) + ((Sum (A /^ i)) + (- (Sum (A /^ i)))) by RLVECT_1:def 6
.= (Sum B) + (0. (Polynom-Ring n,L)) by RLVECT_1:16
.= Sum B by RLVECT_1:def 7 ;
then A3: Sum B = (Sum A) - (Sum (A /^ i)) by RLVECT_1:def 12
.= f - g by A1, A2, Lm3 ;
dom (A | (Seg i)) c= dom A by RELAT_1:89;
then A4: dom B c= dom A by A1, FINSEQ_1:def 15;

now

let j be Element of NAT ; :: thesis: ( j in dom B implies ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B /. j = m *' p & HT (m *' p),T <= b,T ) )
assume A5: j in dom B ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B /. j = m *' p & HT (m *' p),T <= b,T )
then A6: j in dom (A | (Seg i)) by A1, FINSEQ_1:def 15;
A7: A /. j = A . j by A4, A5, PARTFUN1:def 8
.= (A | (Seg i)) . j by A6, FUNCT_1:70
.= B . j by A1, FINSEQ_1:def 15
.= B /. j by A5, PARTFUN1:def 8 ;
consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A8: ( p in P & A /. j = m *' p & HT (m *' p),T <= b,T ) by A1, A4, A5, Def7;
thus ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B /. j = m *' p & HT (m *' p),T <= b,T ) by A7, A8; :: thesis: verum

end;

hence B is_Standard_Representation_of f - g,P,b,T by A3, Def7; :: thesis: verum