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 n

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 n

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 n

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 n

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 n

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 n

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 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) 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 that

A1: A is_Standard_Representation_of f,P,b,T and

A2: B = A | i and

A3: g = Sum (A /^ i) ; :: thesis: B is_Standard_Representation_of f - g,P,b,T

A4: Sum A = f by A1;

dom (A | (Seg i)) c= dom A by RELAT_1:60;

then A5: dom B c= dom A by A2, FINSEQ_1:def 15;

then Sum A = (Sum B) + (Sum (A /^ i)) by RLVECT_1:41;

then (Sum A) + (- (Sum (A /^ i))) = (Sum B) + ((Sum (A /^ i)) + (- (Sum (A /^ i)))) by RLVECT_1:def 3

.= (Sum B) + (0. (Polynom-Ring (n,L))) by RLVECT_1:5

.= Sum B by RLVECT_1:def 4 ;

then Sum B = (Sum A) - (Sum (A /^ i))

.= f - g by A3, A4, Lm3 ;

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

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 n

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 n

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 n

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 n

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 n

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 n

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 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) 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 that

A1: A is_Standard_Representation_of f,P,b,T and

A2: B = A | i and

A3: g = Sum (A /^ i) ; :: thesis: B is_Standard_Representation_of f - g,P,b,T

A4: Sum A = f by A1;

dom (A | (Seg i)) c= dom A by RELAT_1:60;

then A5: dom B c= dom A by A2, FINSEQ_1:def 15;

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 )

A = B ^ (A /^ i)
by A2, RFINSEQ:8;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 in dom (A | (Seg i)) by A2, FINSEQ_1:def 15;

A /. j = A . j by A5, A7, PARTFUN1:def 6

.= (A | (Seg i)) . j by A8, FUNCT_1:47

.= B . j by A2, FINSEQ_1:def 15

.= B /. j by A7, 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, A5, A7; :: thesis: verum

end;( 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 in dom (A | (Seg i)) by A2, FINSEQ_1:def 15;

A /. j = A . j by A5, A7, PARTFUN1:def 6

.= (A | (Seg i)) . j by A8, FUNCT_1:47

.= B . j by A2, FINSEQ_1:def 15

.= B /. j by A7, 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, A5, A7; :: thesis: verum

then Sum A = (Sum B) + (Sum (A /^ i)) by RLVECT_1:41;

then (Sum A) + (- (Sum (A /^ i))) = (Sum B) + ((Sum (A /^ i)) + (- (Sum (A /^ i)))) by RLVECT_1:def 3

.= (Sum B) + (0. (Polynom-Ring (n,L))) by RLVECT_1:5

.= Sum B by RLVECT_1:def 4 ;

then Sum B = (Sum A) - (Sum (A /^ i))

.= f - g by A3, A4, Lm3 ;

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