let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive Abelian 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) & i <= len A 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 Abelian 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) & i <= len A holds
B is_Standard_Representation_of f - g,P,b,T
let L be non empty non trivial right_complementable well-unital distributive Abelian 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) & i <= len A 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) & i <= len A 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) & i <= len A 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) & i <= len A 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) & i <= len A 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) & i <= len A 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) & i <= len A ) ; :: 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 = (A | i) ^ B by A1, RFINSEQ:21;
then Sum A = (Sum (A | i)) + (Sum B) by RLVECT_1:58;
then (Sum A) + (- (Sum (A | i))) = ((Sum (A | i)) + (- (Sum (A | i)))) + (Sum B) by RLVECT_1:def 6
.= (0. (Polynom-Ring n,L)) + (Sum B) by RLVECT_1:16
.= Sum B by ALGSTR_1:def 5 ;
then A3: Sum B = (Sum A) - (Sum (A | i)) by RLVECT_1:def 12
.= f - g by A1, A2, Lm3 ;

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 A4: 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 A5: j + i in dom A by A1, FINSEQ_5:29;
A6: B /. j = B . j by A4, PARTFUN1:def 8
.= A . (j + i) by A1, A4, RFINSEQ:def 2
.= A /. (j + i) by A5, PARTFUN1:def 8 ;
consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A7: ( p in P & A /. (j + i) = m *' p & HT (m *' p),T <= b,T ) by A1, 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 A6, A7; :: thesis: verum

end;

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