let n be Ordinal; 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; 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 ; 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; 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)); 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; ( 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
; 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
; 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
; 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
; ( 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; verum