let n be Ordinal; 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 being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let T be connected TermOrder of n; for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let f be Polynomial of n,L; for P being non empty Subset of (Polynom-Ring (n,L))
for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let P be non empty Subset of (Polynom-Ring (n,L)); for A being LeftLinearCombination of P
for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let A be LeftLinearCombination of P; for b being bag of n st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let b be bag of n; ( A is_Standard_Representation_of f,P,b,T implies A is_MonomialRepresentation_of f )
assume A1:
A is_Standard_Representation_of f,P,b,T
; A is_MonomialRepresentation_of f
A2:
now for i being Element of NAT st i in dom A holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p )let i be
Element of
NAT ;
( i in dom A implies ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p ) )assume
i in dom A
;
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p )then
ex
m9 being
non-zero Monomial of
n,
L ex
p9 being
non-zero Polynomial of
n,
L st
(
p9 in P &
A /. i = m9 *' p9 &
HT (
(m9 *' p9),
T)
<= b,
T )
by A1;
hence
ex
m being
Monomial of
n,
L ex
p being
Polynomial of
n,
L st
(
p in P &
A /. i = m *' p )
;
verum end;
Sum A = f
by A1;
hence
A is_MonomialRepresentation_of f
by A2; verum