let n be Ordinal; 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; 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 ; 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; 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)); 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; 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; 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 ; ( 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
; B is_Standard_Representation_of f - g,P,b,T
A5:
Sum A = f
by A1;
A6:
now 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 ;
( 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
;
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;
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; verum