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

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

for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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

for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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

f is_top_reducible_wrt P,T

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

assume f has_a_Standard_Representation_of P,T ; :: thesis: f is_top_reducible_wrt P,T

then consider A being LeftLinearCombination of P such that

A1: A is_Standard_Representation_of f,P,T ;

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: p in P and

i in dom A and

A /. i = m *' p and

A3: HT (f,T) = HT ((m *' p),T) by A1, Th37;

set s = HT (m,T);

A4: HT (f,T) = (HT (m,T)) + (HT (p,T)) by A3, TERMORD:31;

set g = f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p));

A5: f <> 0_ (n,L) by POLYNOM7:def 1;

then Support f <> {} by POLYNOM7:1;

then ( p <> 0_ (n,L) & HT (f,T) in Support f ) by POLYNOM7:def 1, TERMORD:def 6;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p)),p, HT (f,T),T by A5, A4, POLYRED:def 5;

then f top_reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p)),p,T by POLYRED:def 10;

then f is_top_reducible_wrt p,T by POLYRED:def 11;

hence f is_top_reducible_wrt P,T by A2, POLYRED:def 12; :: thesis: verum

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

for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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

for f being non-zero Polynomial of n,L

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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

for P being non empty Subset of (Polynom-Ring (n,L)) st f has_a_Standard_Representation_of P,T holds

f is_top_reducible_wrt P,T

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

f is_top_reducible_wrt P,T

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

assume f has_a_Standard_Representation_of P,T ; :: thesis: f is_top_reducible_wrt P,T

then consider A being LeftLinearCombination of P such that

A1: A is_Standard_Representation_of f,P,T ;

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: p in P and

i in dom A and

A /. i = m *' p and

A3: HT (f,T) = HT ((m *' p),T) by A1, Th37;

set s = HT (m,T);

A4: HT (f,T) = (HT (m,T)) + (HT (p,T)) by A3, TERMORD:31;

set g = f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p));

A5: f <> 0_ (n,L) by POLYNOM7:def 1;

then Support f <> {} by POLYNOM7:1;

then ( p <> 0_ (n,L) & HT (f,T) in Support f ) by POLYNOM7:def 1, TERMORD:def 6;

then f reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p)),p, HT (f,T),T by A5, A4, POLYRED:def 5;

then f top_reduces_to f - (((f . (HT (f,T))) / (HC (p,T))) * ((HT (m,T)) *' p)),p,T by POLYRED:def 10;

then f is_top_reducible_wrt p,T by POLYRED:def 11;

hence f is_top_reducible_wrt P,T by A2, POLYRED:def 12; :: thesis: verum