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 non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),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 being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let f be non-zero Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f implies ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T ) )

HC (f,T) <> 0. L ;

then A1: f . (HT (f,T)) <> 0. L by TERMORD:def 7;

assume A is_MonomialRepresentation_of f ; :: thesis: ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

then consider i being Element of NAT such that

A2: i in dom A and

A3: ex m being Monomial of n,L ex p being Polynomial of n,L st

( A . i = m *' p & p in P & (m *' p) . (HT (f,T)) <> 0. L ) by A1, Lm4;

consider m being Monomial of n,L, p being Polynomial of n,L such that

A4: A . i = m *' p and

A5: (m *' p) . (HT (f,T)) <> 0. L and

A6: p in P by A3;

A7: m *' p <> 0_ (n,L) by A5, POLYNOM1:22;

then A8: m <> 0_ (n,L) by POLYRED:5;

p <> 0_ (n,L) by A7, POLYNOM1:28;

then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;

reconsider m = m as non-zero Monomial of n,L by A8, POLYNOM7:def 1;

HT (f,T) in Support (m *' p) by A5, POLYNOM1:def 4;

then HT (f,T) <= HT ((m *' p),T),T by TERMORD:def 6;

hence ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T ) by A2, A4, A6; :: thesis: verum

for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),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 being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let f be non-zero Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L))

for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_MonomialRepresentation_of f holds

ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

let A be LeftLinearCombination of P; :: thesis: ( A is_MonomialRepresentation_of f implies ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T ) )

HC (f,T) <> 0. L ;

then A1: f . (HT (f,T)) <> 0. L by TERMORD:def 7;

assume A is_MonomialRepresentation_of f ; :: thesis: ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T )

then consider i being Element of NAT such that

A2: i in dom A and

A3: ex m being Monomial of n,L ex p being Polynomial of n,L st

( A . i = m *' p & p in P & (m *' p) . (HT (f,T)) <> 0. L ) by A1, Lm4;

consider m being Monomial of n,L, p being Polynomial of n,L such that

A4: A . i = m *' p and

A5: (m *' p) . (HT (f,T)) <> 0. L and

A6: p in P by A3;

A7: m *' p <> 0_ (n,L) by A5, POLYNOM1:22;

then A8: m <> 0_ (n,L) by POLYRED:5;

p <> 0_ (n,L) by A7, POLYNOM1:28;

then reconsider p = p as non-zero Polynomial of n,L by POLYNOM7:def 1;

reconsider m = m as non-zero Monomial of n,L by A8, POLYNOM7:def 1;

HT (f,T) in Support (m *' p) by A5, POLYNOM1:def 4;

then HT (f,T) <= HT ((m *' p),T),T by TERMORD:def 6;

hence ex i being Element of NAT ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

( i in dom A & p in P & A . i = m *' p & HT (f,T) <= HT ((m *' p),T),T ) by A2, A4, A6; :: thesis: verum