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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ B is_Standard_Representation_of f + g,P,b,T

let A, B be LeftLinearCombination of P; :: thesis: for b being bag of n st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ B is_Standard_Representation_of f + g,P,b,T

let b be bag of n; :: thesis: ( A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T implies A ^ 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 is_Standard_Representation_of g,P,b,T ; :: thesis: A ^ B is_Standard_Representation_of f + g,P,b,T

then f + g = (Sum A) + (Sum B) by POLYNOM1:def 11

.= Sum (A ^ B) by RLVECT_1:41 ;

hence A ^ B is_Standard_Representation_of f + g,P,b,T by A3; :: 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ 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 st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ B is_Standard_Representation_of f + g,P,b,T

let A, B be LeftLinearCombination of P; :: thesis: for b being bag of n st A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T holds

A ^ B is_Standard_Representation_of f + g,P,b,T

let b be bag of n; :: thesis: ( A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T implies A ^ 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 is_Standard_Representation_of g,P,b,T ; :: thesis: A ^ B is_Standard_Representation_of f + g,P,b,T

A3: now :: thesis: for i being Element of NAT st i in dom (A ^ B) holds

ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

( f = Sum A & g = Sum B )
by A1, A2;ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

let i be Element of NAT ; :: thesis: ( i in dom (A ^ B) implies ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) )

assume A4: i in dom (A ^ B) ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) ; :: thesis: verum

end;( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) )

assume A4: i in dom (A ^ B) ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

now :: thesis: ( ( i in dom A & ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) ) or ( ex k being Nat st

( k in dom B & i = (len A) + k ) & ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) ) )end;

hence
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st ( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) ) or ( ex k being Nat st

( k in dom B & i = (len A) + k ) & ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) ) )

per cases
( i in dom A or ex k being Nat st

( k in dom B & i = (len A) + k ) ) by A4, FINSEQ_1:25;

end;

( k in dom B & i = (len A) + k ) ) by A4, FINSEQ_1:25;

case A5:
i in dom A
; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

(A ^ B) /. i =
(A ^ B) . i
by A4, PARTFUN1:def 6

.= A . i by A5, FINSEQ_1:def 7

.= A /. i by A5, 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 & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) by A1, A5; :: thesis: verum

end;.= A . i by A5, FINSEQ_1:def 7

.= A /. i by A5, 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 & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) by A1, A5; :: thesis: verum

case
ex k being Nat st

( k in dom B & i = (len A) + k ) ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

( k in dom B & i = (len A) + k ) ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T )

then consider k being Nat such that

A6: k in dom B and

A7: i = (len A) + k ;

(A ^ B) /. i = (A ^ B) . i by A4, PARTFUN1:def 6

.= B . k by A6, A7, FINSEQ_1:def 7

.= B /. k by A6, 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 & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) by A2, A6; :: thesis: verum

end;A6: k in dom B and

A7: i = (len A) + k ;

(A ^ B) /. i = (A ^ B) . i by A4, PARTFUN1:def 6

.= B . k by A6, A7, FINSEQ_1:def 7

.= B /. k by A6, 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 & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) by A2, A6; :: thesis: verum

( p in P & (A ^ B) /. i = m *' p & HT ((m *' p),T) <= b,T ) ; :: thesis: verum

then f + g = (Sum A) + (Sum B) by POLYNOM1:def 11

.= Sum (A ^ B) by RLVECT_1:41 ;

hence A ^ B is_Standard_Representation_of f + g,P,b,T by A3; :: thesis: verum