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 by Def8;
then A is_MonomialRepresentation_of f by Th37;
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 & p in P & A . i = m *' p & HT f,T <= HT (m *' p),T,T ) by Th41;
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 <= HT f,T,T ) by A1, A2, Def7;
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 m' ; :: thesis: 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 p' ; :: thesis: ( p' in P & i in dom A & A /. i = m' *' p' & HT f,T = HT (m' *' p'),T )
m *' p = m' *' p' by A2, A3, PARTFUN1:def 8;
hence ( p' in P & i in dom A & A /. i = m' *' p' & HT f,T = HT (m' *' p'),T ) by A2, A3, TERMORD:7; :: thesis: verum