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 n 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 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 ; :: 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 n 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 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)); :: thesis: 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; :: thesis: 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; :: 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

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

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; :: 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 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 ; :: 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 n 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 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)); :: thesis: 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; :: thesis: 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; :: 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

A2: now :: thesis: 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 )

Sum A = f
by A1;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 ; :: 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 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 ) ; :: thesis: verum

end;( 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 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 ) ; :: thesis: verum

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