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 n
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 n
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 n
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 n
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 n
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 n
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 n; :: 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 that
A1: A is_Standard_Representation_of f,P,b,T and
A2: B = A /^ i and
A3: g = Sum (A | i) and
A4: i <= len A ; :: thesis: B is_Standard_Representation_of f - g,P,b,T
A5: Sum A = f by A1;

A6: now :: thesis: for j being Element of NAT st j in dom B holds
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 )

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 A7: 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 A8: j + i in dom A by A2, FINSEQ_5:26;
B /. j = B . j by A7, PARTFUN1:def 6
.= A . (j + i) by A2, A4, A7, RFINSEQ:def 1
.= A /. (j + i) by A8, PARTFUN1:def 6 ;
hence 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 A1, A8; :: thesis: verum

end;

A = (A | i) ^ B by A2, RFINSEQ:8;
then Sum A = (Sum (A | i)) + (Sum B) by RLVECT_1:41;
then (Sum A) + (- (Sum (A | i))) = ((Sum (A | i)) + (- (Sum (A | i)))) + (Sum B) by RLVECT_1:def 3
.= (0. (Polynom-Ring (n,L))) + (Sum B) by RLVECT_1:5
.= Sum B by ALGSTR_1:def 2 ;
then Sum B = (Sum A) - (Sum (A | i))
.= f - g by A3, A5, Lm3 ;
hence B is_Standard_Representation_of f - g,P,b,T by A6; :: thesis: verum