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 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 st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
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 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 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 ; :: thesis: 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 st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring n,L)
for A being LeftLinearCombination of P
for b being bag of 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); :: thesis: for A being LeftLinearCombination of P
for b being bag of st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let A be LeftLinearCombination of P; :: thesis: for b being bag of st A is_Standard_Representation_of f,P,b,T holds
A is_MonomialRepresentation_of f
let b be bag of ; :: thesis: ( 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 ; :: thesis: A is_MonomialRepresentation_of f
then A2: ( Sum A = f & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A /. i = m *' p & HT (m *' p),T <= b,T ) ) ) by Def7;

now

let i be Element of NAT ; :: thesis: ( 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 ; :: thesis: ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p )
then consider m' being non-zero Monomial of n,L, p' being non-zero Polynomial of n,L such that
A3: ( p' in P & A /. i = m' *' p' & HT (m' *' p'),T <= b,T ) by A1, Def7;
thus ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p ) by A3; :: thesis: verum

end;

hence A is_MonomialRepresentation_of f by A2, Def6; :: thesis: verum