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 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 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 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 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 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 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 ; :: 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 A1:
( A is_Standard_Representation_of f,P,b,T & B is_Standard_Representation_of g,P,b,T )
; :: thesis: A ^ B is_Standard_Representation_of f + g,P,b,T
then
( f = Sum A & g = Sum B )
by Def7;
then A2: f + g =
(Sum A) + (Sum B)
by POLYNOM1:def 27
.=
Sum (A ^ B)
by RLVECT_1:58
;
now 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 A3:
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 per cases
( i in dom A or ex k being Nat st
( k in dom B & i = (len A) + k ) )
by A3, FINSEQ_1:38;
case A4:
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 )then consider m being
non-zero Monomial of
n,
L,
p being
non-zero Polynomial of
n,
L such that A5:
(
p in P &
A /. i = m *' p &
HT (m *' p),
T <= b,
T )
by A1, Def7;
(A ^ B) /. i =
(A ^ B) . i
by A3, PARTFUN1:def 8
.=
A . i
by A4, FINSEQ_1:def 7
.=
A /. i
by A4, PARTFUN1:def 8
;
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 A5;
:: thesis: verum end; 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 )then consider k being
Nat such that A6:
(
k in dom B &
i = (len A) + k )
;
consider m being
non-zero Monomial of
n,
L,
p being
non-zero Polynomial of
n,
L such that A7:
(
p in P &
B /. k = m *' p &
HT (m *' p),
T <= b,
T )
by A1, A6, Def7;
(A ^ B) /. i =
(A ^ B) . i
by A3, PARTFUN1:def 8
.=
B . k
by A6, FINSEQ_1:def 7
.=
B /. k
by A6, PARTFUN1:def 8
;
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 A7;
:: thesis: verum 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 )
;
:: thesis: verum end;
hence
A ^ B is_Standard_Representation_of f + g,P,b,T
by A2, Def7; :: thesis: verum