let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

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

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( PolyRedRel (P,T) reduces f, 0_ (n,L) implies f has_a_Standard_Representation_of P,T )

reconsider f9 = f as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

assume PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: f has_a_Standard_Representation_of P,T

then consider A being LeftLinearCombination of P such that

A2: f9 = (0. (Polynom-Ring (n,L))) + (Sum A) and

A3: for i being Element of NAT st i in dom A holds

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

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

then A is_Standard_Representation_of f,P, HT (f,T),T by A4;

then A is_Standard_Representation_of f,P,T ;

hence f has_a_Standard_Representation_of P,T ; :: thesis: verum

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for f being Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

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

for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

let f be Polynomial of n,L; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f, 0_ (n,L) holds

f has_a_Standard_Representation_of P,T

let P be non empty Subset of (Polynom-Ring (n,L)); :: thesis: ( PolyRedRel (P,T) reduces f, 0_ (n,L) implies f has_a_Standard_Representation_of P,T )

reconsider f9 = f as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

assume PolyRedRel (P,T) reduces f, 0_ (n,L) ; :: thesis: f has_a_Standard_Representation_of P,T

then consider A being LeftLinearCombination of P such that

A2: f9 = (0. (Polynom-Ring (n,L))) + (Sum A) and

A3: for i being Element of NAT st i in dom A holds

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

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

A4: now :: thesis: for i being Element of NAT st i in dom A holds

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

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

f = Sum A
by A2, RLVECT_1:def 4;ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

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

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

assume A5: i in dom A ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

then ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

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

( p in P & A /. i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by A5, PARTFUN1:def 6; :: thesis: verum

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

assume A5: i in dom A ; :: thesis: ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

then ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st

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

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

( p in P & A /. i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by A5, PARTFUN1:def 6; :: thesis: verum

then A is_Standard_Representation_of f,P, HT (f,T),T by A4;

then A is_Standard_Representation_of f,P,T ;

hence f has_a_Standard_Representation_of P,T ; :: thesis: verum