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_Standard_Representation_of f,P,T 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

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),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_Standard_Representation_of f,P,T 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

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),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_Standard_Representation_of f,P,T 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

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),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_Standard_Representation_of f,P,T 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

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

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T 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

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

let A be LeftLinearCombination of P; :: thesis: ( A is_Standard_Representation_of f,P,T 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

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

assume A is_Standard_Representation_of f,P,T ; :: 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

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

then A1: A is_Standard_Representation_of f,P, HT (f,T),T ;

then consider i being Element of NAT , m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that

A2: i in dom A and

p in P and

A3: A . i = m *' p and

A4: HT (f,T) <= HT ((m *' p),T),T by Th32, Th36;

consider m9 being non-zero Monomial of n,L, p9 being non-zero Polynomial of n,L such that

A5: p9 in P and

A6: A /. i = m9 *' p9 and

A7: HT ((m9 *' p9),T) <= HT (f,T),T by A1, A2;

take i ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

take m9 ; :: thesis: ex p being non-zero Polynomial of n,L st

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

take p9 ; :: thesis: ( p9 in P & i in dom A & A /. i = m9 *' p9 & HT (f,T) = HT ((m9 *' p9),T) )

m *' p = m9 *' p9 by A2, A3, A6, PARTFUN1:def 6;

hence ( p9 in P & i in dom A & A /. i = m9 *' p9 & HT (f,T) = HT ((m9 *' p9),T) ) by A2, A4, A5, A6, A7, TERMORD:7; :: 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_Standard_Representation_of f,P,T 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

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),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_Standard_Representation_of f,P,T 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

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),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_Standard_Representation_of f,P,T 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

( p in P & i in dom A & A /. i = m *' p & HT (f,T) = HT ((m *' p),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_Standard_Representation_of f,P,T 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

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

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: for A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T 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

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

let A be LeftLinearCombination of P; :: thesis: ( A is_Standard_Representation_of f,P,T 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

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

assume A is_Standard_Representation_of f,P,T ; :: 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

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

then A1: A is_Standard_Representation_of f,P, HT (f,T),T ;

then consider i being Element of NAT , m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that

A2: i in dom A and

p in P and

A3: A . i = m *' p and

A4: HT (f,T) <= HT ((m *' p),T),T by Th32, Th36;

consider m9 being non-zero Monomial of n,L, p9 being non-zero Polynomial of n,L such that

A5: p9 in P and

A6: A /. i = m9 *' p9 and

A7: HT ((m9 *' p9),T) <= HT (f,T),T by A1, A2;

take i ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

take m9 ; :: thesis: ex p being non-zero Polynomial of n,L st

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

take p9 ; :: thesis: ( p9 in P & i in dom A & A /. i = m9 *' p9 & HT (f,T) = HT ((m9 *' p9),T) )

m *' p = m9 *' p9 by A2, A3, A6, PARTFUN1:def 6;

hence ( p9 in P & i in dom A & A /. i = m9 *' p9 & HT (f,T) = HT ((m9 *' p9),T) ) by A2, A4, A5, A6, A7, TERMORD:7; :: thesis: verum