let n be Element of NAT ; :: 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 I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds

ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt 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 I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds

ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt 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 I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds

ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: ( I <> {(0_ (n,L))} implies ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt T ) )

set R = RelStr(# (Bags n),(DivOrder n) #);

assume A1: I <> {(0_ (n,L))} ; :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

ex q being Element of I st q <> 0_ (n,L)

A5: q <> 0_ (n,L) ;

reconsider q = q as Polynomial of n,L by POLYNOM1:def 11;

HT (q,T) in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A5;

then reconsider hti = HT (I,T) as non empty Subset of RelStr(# (Bags n),(DivOrder n) #) ;

set hq = HT (q,T);

consider S being set such that

A6: S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) and

A7: for C being set st C is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) holds

S c= C by DICKSON:34;

reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

set M = { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } ;

set s = the Element of S;

hq in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A5;

then A11: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S & b <= hq ) by A6, DICKSON:def 9;

then the Element of S in S ;

then reconsider s = the Element of S as Element of Bags n ;

{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for r being Polynomial of n,L holds

( not r in I or not r < p,T or not r <> 0_ (n,L) or not HM (r,T) = Monom ((1. L),s) ) ) ) } in { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } by A11;

then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } as non empty set ;

set G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ;

A12: for x being set st x in M holds

ex q being Polynomial of n,L st

( q in I & x = {q} & q <> 0_ (n,L) )

A46: M is finite

G <> {}

take G ; :: thesis: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

for b being bag of n st b in HT (I,T) holds

ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

hence G is_Groebner_basis_of I,T by A45, Th29; :: thesis: G is_reduced_wrt T

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

for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds

ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt 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 I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds

ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt 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 I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds

ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: ( I <> {(0_ (n,L))} implies ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt T ) )

set R = RelStr(# (Bags n),(DivOrder n) #);

assume A1: I <> {(0_ (n,L))} ; :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st

( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

ex q being Element of I st q <> 0_ (n,L)

proof

then consider q being Element of I such that
assume A2:
for q being Element of I holds not q <> 0_ (n,L)
; :: thesis: contradiction

end;A3: now :: thesis: for u being object st u in {(0_ (n,L))} holds

u in I

u in I

let u be object ; :: thesis: ( u in {(0_ (n,L))} implies u in I )

assume u in {(0_ (n,L))} ; :: thesis: u in I

then A4: u = 0_ (n,L) by TARSKI:def 1;

end;assume u in {(0_ (n,L))} ; :: thesis: u in I

then A4: u = 0_ (n,L) by TARSKI:def 1;

now :: thesis: u in I

hence
u in I
; :: thesis: verumassume
not u in I
; :: thesis: contradiction

then for v being object holds not v in I by A2, A4;

hence contradiction by XBOOLE_0:def 1; :: thesis: verum

end;then for v being object holds not v in I by A2, A4;

hence contradiction by XBOOLE_0:def 1; :: thesis: verum

now :: thesis: for u being object st u in I holds

u in {(0_ (n,L))}

hence
contradiction
by A1, A3, TARSKI:2; :: thesis: verumu in {(0_ (n,L))}

let u be object ; :: thesis: ( u in I implies u in {(0_ (n,L))} )

assume u in I ; :: thesis: u in {(0_ (n,L))}

then u = 0_ (n,L) by A2;

hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis: verum

end;assume u in I ; :: thesis: u in {(0_ (n,L))}

then u = 0_ (n,L) by A2;

hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis: verum

A5: q <> 0_ (n,L) ;

reconsider q = q as Polynomial of n,L by POLYNOM1:def 11;

HT (q,T) in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A5;

then reconsider hti = HT (I,T) as non empty Subset of RelStr(# (Bags n),(DivOrder n) #) ;

set hq = HT (q,T);

consider S being set such that

A6: S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) and

A7: for C being set st C is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) holds

S c= C by DICKSON:34;

reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

A8: now :: thesis: S is finite

A10:
S c= hti
by A6, DICKSON:def 9;A9:
ex B being set st

( B is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) & B is finite ) by DICKSON:def 10;

assume not S is finite ; :: thesis: contradiction

hence contradiction by A7, A9, FINSET_1:1; :: thesis: verum

end;( B is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) & B is finite ) by DICKSON:def 10;

assume not S is finite ; :: thesis: contradiction

hence contradiction by A7, A9, FINSET_1:1; :: thesis: verum

now :: thesis: for u being object st u in S holds

u in Bags n

then reconsider S = S as finite Subset of (Bags n) by A8, TARSKI:def 3;u in Bags n

let u be object ; :: thesis: ( u in S implies u in Bags n )

assume u in S ; :: thesis: u in Bags n

then u in hti by A10;

hence u in Bags n ; :: thesis: verum

end;assume u in S ; :: thesis: u in Bags n

then u in hti by A10;

hence u in Bags n ; :: thesis: verum

set M = { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } ;

set s = the Element of S;

hq in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A5;

then A11: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S & b <= hq ) by A6, DICKSON:def 9;

then the Element of S in S ;

then reconsider s = the Element of S as Element of Bags n ;

{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for r being Polynomial of n,L holds

( not r in I or not r < p,T or not r <> 0_ (n,L) or not HM (r,T) = Monom ((1. L),s) ) ) ) } in { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } by A11;

then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } where s is Element of Bags n : s in S } as non empty set ;

set G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ;

A12: for x being set st x in M holds

ex q being Polynomial of n,L st

( q in I & x = {q} & q <> 0_ (n,L) )

proof

let x be set ; :: thesis: ( x in M implies ex q being Polynomial of n,L st

( q in I & x = {q} & q <> 0_ (n,L) ) )

assume x in M ; :: thesis: ex q being Polynomial of n,L st

( q in I & x = {q} & q <> 0_ (n,L) )

then consider s being Element of Bags n such that

A13: x = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } and

A14: s in S ;

s in hti by A10, A14;

then consider q being Polynomial of n,L such that

A15: s = HT (q,T) and

A16: ( q in I & q <> 0_ (n,L) ) ;

consider qq being Polynomial of n,L such that

A17: ( qq in I & HM (qq,T) = Monom ((1. L),(HT (q,T))) & qq <> 0_ (n,L) ) by A16, Lm10;

set M9 = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } ;

then reconsider M9 = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } as non empty Subset of (Polynom-Ring (n,L)) by A18, TARSKI:def 3;

reconsider M9 = M9 as non empty Subset of (Polynom-Ring (n,L)) ;

consider p being Polynomial of n,L such that

A19: p in M9 and

A20: for r being Polynomial of n,L st r in M9 holds

p <= r,T by POLYRED:31;

consider p9 being Polynomial of n,L such that

A21: p9 = p and

A22: p9 in I and

A23: HM (p9,T) = Monom ((1. L),s) and

A24: p9 <> 0_ (n,L) by A19;

p9 in x by A13, A22, A23, A24, A25;

then for u being object st u in {p9} holds

u in x by TARSKI:def 1;

hence ( p9 in I & x = {p9} & p9 <> 0_ (n,L) ) by A22, A24, A33, TARSKI:2; :: thesis: verum

end;( q in I & x = {q} & q <> 0_ (n,L) ) )

assume x in M ; :: thesis: ex q being Polynomial of n,L st

( q in I & x = {q} & q <> 0_ (n,L) )

then consider s being Element of Bags n such that

A13: x = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } and

A14: s in S ;

s in hti by A10, A14;

then consider q being Polynomial of n,L such that

A15: s = HT (q,T) and

A16: ( q in I & q <> 0_ (n,L) ) ;

consider qq being Polynomial of n,L such that

A17: ( qq in I & HM (qq,T) = Monom ((1. L),(HT (q,T))) & qq <> 0_ (n,L) ) by A16, Lm10;

set M9 = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } ;

A18: now :: thesis: for u being object st u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } holds

u in the carrier of (Polynom-Ring (n,L))

qq in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) }
by A15, A17;u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ex pp being Polynomial of n,L st

( u = pp & pp in I & HM (pp,T) = Monom ((1. L),s) & pp <> 0_ (n,L) ) ;

hence u in the carrier of (Polynom-Ring (n,L)) ; :: thesis: verum

end;assume u in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ex pp being Polynomial of n,L st

( u = pp & pp in I & HM (pp,T) = Monom ((1. L),s) & pp <> 0_ (n,L) ) ;

hence u in the carrier of (Polynom-Ring (n,L)) ; :: thesis: verum

then reconsider M9 = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) ) } as non empty Subset of (Polynom-Ring (n,L)) by A18, TARSKI:def 3;

reconsider M9 = M9 as non empty Subset of (Polynom-Ring (n,L)) ;

consider p being Polynomial of n,L such that

A19: p in M9 and

A20: for r being Polynomial of n,L st r in M9 holds

p <= r,T by POLYRED:31;

consider p9 being Polynomial of n,L such that

A21: p9 = p and

A22: p9 in I and

A23: HM (p9,T) = Monom ((1. L),s) and

A24: p9 <> 0_ (n,L) by A19;

A25: now :: thesis: for q being Polynomial of n,L holds

( not q in I or not q < p9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) )

( not q in I or not q < p9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) )

assume
ex q being Polynomial of n,L st

( q in I & q < p9,T & q <> 0_ (n,L) & HM (q,T) = Monom ((1. L),s) ) ; :: thesis: contradiction

then consider q being Polynomial of n,L such that

A26: q in I and

A27: q < p9,T and

A28: ( q <> 0_ (n,L) & HM (q,T) = Monom ((1. L),s) ) ;

q in M9 by A26, A28;

then p <= q,T by A20;

hence contradiction by A21, A27, POLYRED:29; :: thesis: verum

end;( q in I & q < p9,T & q <> 0_ (n,L) & HM (q,T) = Monom ((1. L),s) ) ; :: thesis: contradiction

then consider q being Polynomial of n,L such that

A26: q in I and

A27: q < p9,T and

A28: ( q <> 0_ (n,L) & HM (q,T) = Monom ((1. L),s) ) ;

q in M9 by A26, A28;

then p <= q,T by A20;

hence contradiction by A21, A27, POLYRED:29; :: thesis: verum

A29: now :: thesis: for q being Polynomial of n,L holds

( not q in I or not q < p9,T or not HM (q,T) = Monom ((1. L),s) )

( not q in I or not q < p9,T or not HM (q,T) = Monom ((1. L),s) )

A30:
1. L <> 0. L
;

assume ex q being Polynomial of n,L st

( q in I & q < p9,T & HM (q,T) = Monom ((1. L),s) ) ; :: thesis: contradiction

then consider q being Polynomial of n,L such that

A31: ( q in I & q < p9,T ) and

A32: HM (q,T) = Monom ((1. L),s) ;

HC (q,T) = coefficient (Monom ((1. L),s)) by A32, TERMORD:22

.= 1. L by POLYNOM7:9 ;

then q <> 0_ (n,L) by A30, TERMORD:17;

hence contradiction by A25, A31, A32; :: thesis: verum

end;assume ex q being Polynomial of n,L st

( q in I & q < p9,T & HM (q,T) = Monom ((1. L),s) ) ; :: thesis: contradiction

then consider q being Polynomial of n,L such that

A31: ( q in I & q < p9,T ) and

A32: HM (q,T) = Monom ((1. L),s) ;

HC (q,T) = coefficient (Monom ((1. L),s)) by A32, TERMORD:22

.= 1. L by POLYNOM7:9 ;

then q <> 0_ (n,L) by A30, TERMORD:17;

hence contradiction by A25, A31, A32; :: thesis: verum

A33: now :: thesis: for u being object st u in x holds

u in {p9}

take
p9
; :: thesis: ( p9 in I & x = {p9} & p9 <> 0_ (n,L) )u in {p9}

let u be object ; :: thesis: ( u in x implies u in {p9} )

assume u in x ; :: thesis: u in {p9}

then consider u9 being Polynomial of n,L such that

A34: u9 = u and

A35: ( u9 in I & HM (u9,T) = Monom ((1. L),s) ) and

u9 <> 0_ (n,L) and

A36: for q being Polynomial of n,L holds

( not q in I or not q < u9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) by A13;

hence u in {p9} by A34, TARSKI:def 1; :: thesis: verum

end;assume u in x ; :: thesis: u in {p9}

then consider u9 being Polynomial of n,L such that

A34: u9 = u and

A35: ( u9 in I & HM (u9,T) = Monom ((1. L),s) ) and

u9 <> 0_ (n,L) and

A36: for q being Polynomial of n,L holds

( not q in I or not q < u9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) by A13;

now :: thesis: for q being Polynomial of n,L holds

( not q in I or not q < u9,T or not HM (q,T) = Monom ((1. L),s) )

then
u9 = p9
by A22, A23, A29, A35, Th37;( not q in I or not q < u9,T or not HM (q,T) = Monom ((1. L),s) )

A37:
1. L <> 0. L
;

assume ex q being Polynomial of n,L st

( q in I & q < u9,T & HM (q,T) = Monom ((1. L),s) ) ; :: thesis: contradiction

then consider q being Polynomial of n,L such that

A38: ( q in I & q < u9,T ) and

A39: HM (q,T) = Monom ((1. L),s) ;

HC (q,T) = coefficient (Monom ((1. L),s)) by A39, TERMORD:22

.= 1. L by POLYNOM7:9 ;

then q <> 0_ (n,L) by A37, TERMORD:17;

hence contradiction by A36, A38, A39; :: thesis: verum

end;assume ex q being Polynomial of n,L st

( q in I & q < u9,T & HM (q,T) = Monom ((1. L),s) ) ; :: thesis: contradiction

then consider q being Polynomial of n,L such that

A38: ( q in I & q < u9,T ) and

A39: HM (q,T) = Monom ((1. L),s) ;

HC (q,T) = coefficient (Monom ((1. L),s)) by A39, TERMORD:22

.= 1. L by POLYNOM7:9 ;

then q <> 0_ (n,L) by A37, TERMORD:17;

hence contradiction by A36, A38, A39; :: thesis: verum

hence u in {p9} by A34, TARSKI:def 1; :: thesis: verum

p9 in x by A13, A22, A23, A24, A25;

then for u being object st u in {p9} holds

u in x by TARSKI:def 1;

hence ( p9 in I & x = {p9} & p9 <> 0_ (n,L) ) by A22, A24, A33, TARSKI:2; :: thesis: verum

now :: thesis: for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds

u in I

then A45:
{ r where r is Polynomial of n,L : ex x being Element of M st x = {r} } c= I
;u in I

let u be object ; :: thesis: ( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in I )

assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in I

then consider r being Polynomial of n,L such that

A40: u = r and

A41: ex x being Element of M st x = {r} ;

consider x being Element of M such that

A42: x = {r} by A41;

consider r9 being Polynomial of n,L such that

A43: r9 in I and

A44: x = {r9} and

r9 <> 0_ (n,L) by A12;

r9 in {r} by A42, A44, TARSKI:def 1;

hence u in I by A40, A43, TARSKI:def 1; :: thesis: verum

end;assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in I

then consider r being Polynomial of n,L such that

A40: u = r and

A41: ex x being Element of M st x = {r} ;

consider x being Element of M such that

A42: x = {r} by A41;

consider r9 being Polynomial of n,L such that

A43: r9 in I and

A44: x = {r9} and

r9 <> 0_ (n,L) by A12;

r9 in {r} by A42, A44, TARSKI:def 1;

hence u in I by A40, A43, TARSKI:def 1; :: thesis: verum

A46: M is finite

proof

A59:
{ r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite
defpred S_{1}[ object , object ] means $2 = { p where p is Polynomial of n,L : ex b being bag of n st

( b = $1 & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } ;

A47: for x being object st x in S holds

ex y being object st S_{1}[x,y]
;

consider f being Function such that

A48: ( dom f = S & ( for x being object st x in S holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A47);

hence M is finite by A48, FINSET_1:8; :: thesis: verum

end;( b = $1 & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } ;

A47: for x being object st x in S holds

ex y being object st S

consider f being Function such that

A48: ( dom f = S & ( for x being object st x in S holds

S

A49: now :: thesis: for u being object st u in rng f holds

u in M

u in M

let u be object ; :: thesis: ( u in rng f implies u in M )

assume u in rng f ; :: thesis: u in M

then consider s being object such that

A50: s in dom f and

A51: u = f . s by FUNCT_1:def 3;

reconsider s = s as Element of Bags n by A48, A50;

set V = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ;

A52: ex b being bag of n st f . s = { p where p is Polynomial of n,L : ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } by A48, A50;

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } by A51, A53, TARSKI:2;

hence u in M by A48, A50; :: thesis: verum

end;assume u in rng f ; :: thesis: u in M

then consider s being object such that

A50: s in dom f and

A51: u = f . s by FUNCT_1:def 3;

reconsider s = s as Element of Bags n by A48, A50;

set V = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ;

A52: ex b being bag of n st f . s = { p where p is Polynomial of n,L : ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } by A48, A50;

A53: now :: thesis: for v being object st v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } holds

v in f . s

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } holds

v in f . s

let v be object ; :: thesis: ( v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } implies v in f . s )

assume v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ; :: thesis: v in f . s

then ex p being Polynomial of n,L st

( v = p & p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) ;

hence v in f . s by A52; :: thesis: verum

end;( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } implies v in f . s )

assume v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ; :: thesis: v in f . s

then ex p being Polynomial of n,L st

( v = p & p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) ;

hence v in f . s by A52; :: thesis: verum

now :: thesis: for v being object st v in f . s holds

v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }

then
u = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }

let v be object ; :: thesis: ( v in f . s implies v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } )

assume v in f . s ; :: thesis: v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }

then ex p being Polynomial of n,L st

( v = p & ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) ) by A52;

hence v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ; :: thesis: verum

end;( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } )

assume v in f . s ; :: thesis: v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) }

then ex p being Polynomial of n,L st

( v = p & ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) ) by A52;

hence v in { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } ; :: thesis: verum

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } by A51, A53, TARSKI:2;

hence u in M by A48, A50; :: thesis: verum

now :: thesis: for u being object st u in M holds

u in rng f

then
rng f = M
by A49, TARSKI:2;u in rng f

let u be object ; :: thesis: ( u in M implies u in rng f )

reconsider uu = u as set by TARSKI:1;

assume u in M ; :: thesis: u in rng f

then consider s being Element of Bags n such that

A54: u = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } and

A55: s in S ;

A56: ex b being bag of n st f . s = { p where p is Polynomial of n,L : ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } by A48, A55;

hence u in rng f by A57, A58, TARSKI:2; :: thesis: verum

end;reconsider uu = u as set by TARSKI:1;

assume u in M ; :: thesis: u in rng f

then consider s being Element of Bags n such that

A54: u = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } and

A55: s in S ;

A56: ex b being bag of n st f . s = { p where p is Polynomial of n,L : ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) } by A48, A55;

A57: now :: thesis: for v being object st v in uu holds

v in f . s

v in f . s

let v be object ; :: thesis: ( v in uu implies v in f . s )

assume v in uu ; :: thesis: v in f . s

then ex p being Polynomial of n,L st

( v = p & p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) by A54;

hence v in f . s by A56; :: thesis: verum

end;assume v in uu ; :: thesis: v in f . s

then ex p being Polynomial of n,L st

( v = p & p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) by A54;

hence v in f . s by A56; :: thesis: verum

A58: now :: thesis: for v being object st v in f . s holds

v in uu

f . s in rng f
by A48, A55, FUNCT_1:3;v in uu

let v be object ; :: thesis: ( v in f . s implies v in uu )

assume v in f . s ; :: thesis: v in uu

then ex p being Polynomial of n,L st

( v = p & ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) ) by A56;

hence v in uu by A54; :: thesis: verum

end;assume v in f . s ; :: thesis: v in uu

then ex p being Polynomial of n,L st

( v = p & ex b being bag of n st

( b = s & p in I & HM (p,T) = Monom ((1. L),b) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b) ) ) ) ) by A56;

hence v in uu by A54; :: thesis: verum

hence u in rng f by A57, A58, TARSKI:2; :: thesis: verum

hence M is finite by A48, FINSET_1:8; :: thesis: verum

proof

defpred S_{1}[ object , object ] means ex p being Polynomial of n,L ex x being Element of M st

( $1 = x & $2 = p & x = {p} );

A60: for x being object st x in M holds

ex y being object st S_{1}[x,y]

A63: ( dom f = M & ( for x being object st x in M holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A60);

hence { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite by A46, A63, FINSET_1:8; :: thesis: verum

end;( $1 = x & $2 = p & x = {p} );

A60: for x being object st x in M holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in M implies ex y being object st S_{1}[x,y] )

assume A61: x in M ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider x9 = x as Element of M ;

consider q being Polynomial of n,L such that

q in I and

A62: x = {q} and

q <> 0_ (n,L) by A12, A61;

take q ; :: thesis: S_{1}[x,q]

take q ; :: thesis: ex x being Element of M st

( x = x & q = q & x = {q} )

take x9 ; :: thesis: ( x = x9 & q = q & x9 = {q} )

thus x = x9 ; :: thesis: ( q = q & x9 = {q} )

thus q = q ; :: thesis: x9 = {q}

thus x9 = {q} by A62; :: thesis: verum

end;assume A61: x in M ; :: thesis: ex y being object st S

then reconsider x9 = x as Element of M ;

consider q being Polynomial of n,L such that

q in I and

A62: x = {q} and

q <> 0_ (n,L) by A12, A61;

take q ; :: thesis: S

take q ; :: thesis: ex x being Element of M st

( x = x & q = q & x = {q} )

take x9 ; :: thesis: ( x = x9 & q = q & x9 = {q} )

thus x = x9 ; :: thesis: ( q = q & x9 = {q} )

thus q = q ; :: thesis: x9 = {q}

thus x9 = {q} by A62; :: thesis: verum

A63: ( dom f = M & ( for x being object st x in M holds

S

A64: now :: thesis: for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds

u in rng f

u in rng f

let u be object ; :: thesis: ( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in rng f )

assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in rng f

then consider r being Polynomial of n,L such that

A65: u = r and

A66: ex x being Element of M st x = {r} ;

consider x being Element of M such that

A67: x = {r} by A66;

S_{1}[x,f . x]
by A63;

then consider p9 being Polynomial of n,L, x9 being Element of M such that

x9 = x and

A68: p9 = f . x and

A69: x = {p9} ;

A70: f . x in rng f by A63, FUNCT_1:3;

p9 in {r} by A67, A69, TARSKI:def 1;

hence u in rng f by A65, A70, A68, TARSKI:def 1; :: thesis: verum

end;assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in rng f

then consider r being Polynomial of n,L such that

A65: u = r and

A66: ex x being Element of M st x = {r} ;

consider x being Element of M such that

A67: x = {r} by A66;

S

then consider p9 being Polynomial of n,L, x9 being Element of M such that

x9 = x and

A68: p9 = f . x and

A69: x = {p9} ;

A70: f . x in rng f by A63, FUNCT_1:3;

p9 in {r} by A67, A69, TARSKI:def 1;

hence u in rng f by A65, A70, A68, TARSKI:def 1; :: thesis: verum

now :: thesis: for u being object st u in rng f holds

u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }

then
rng f = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }
by A64, TARSKI:2;u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }

let u be object ; :: thesis: ( u in rng f implies u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } )

assume u in rng f ; :: thesis: u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }

then consider s being object such that

A71: s in dom f and

A72: u = f . s by FUNCT_1:def 3;

reconsider s = s as Element of M by A63, A71;

ex p9 being Polynomial of n,L ex x9 being Element of M st

( x9 = s & p9 = f . s & x9 = {p9} ) by A63;

hence u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } by A72; :: thesis: verum

end;assume u in rng f ; :: thesis: u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} }

then consider s being object such that

A71: s in dom f and

A72: u = f . s by FUNCT_1:def 3;

reconsider s = s as Element of M by A63, A71;

ex p9 being Polynomial of n,L ex x9 being Element of M st

( x9 = s & p9 = f . s & x9 = {p9} ) by A63;

hence u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } by A72; :: thesis: verum

hence { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } is finite by A46, A63, FINSET_1:8; :: thesis: verum

now :: thesis: for u being object st u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } holds

u in the carrier of (Polynom-Ring (n,L))

then reconsider G = { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ex r being Polynomial of n,L st

( u = r & ex x being Element of M st x = {r} ) ;

hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum

end;assume u in { r where r is Polynomial of n,L : ex x being Element of M st x = {r} } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then ex r being Polynomial of n,L st

( u = r & ex x being Element of M st x = {r} ) ;

hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum

G <> {}

proof

then reconsider G = G as non empty finite Subset of (Polynom-Ring (n,L)) by A59;
set z = the Element of M;

consider r being Polynomial of n,L such that

r in I and

A73: the Element of M = {r} and

r <> 0_ (n,L) by A12;

r in G by A73;

hence G <> {} ; :: thesis: verum

end;consider r being Polynomial of n,L such that

r in I and

A73: the Element of M = {r} and

r <> 0_ (n,L) by A12;

r in G by A73;

hence G <> {} ; :: thesis: verum

take G ; :: thesis: ( G is_Groebner_basis_of I,T & G is_reduced_wrt T )

for b being bag of n st b in HT (I,T) holds

ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

proof

then
HT (I,T) c= multiples (HT (G,T))
by Th28;
let b be bag of n; :: thesis: ( b in HT (I,T) implies ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b ) )

reconsider bb = b as Element of RelStr(# (Bags n),(DivOrder n) #) by PRE_POLY:def 12;

assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

then consider bb9 being Element of RelStr(# (Bags n),(DivOrder n) #) such that

A74: bb9 in S and

A75: bb9 <= bb by A6, DICKSON:def 9;

A76: [bb9,bb] in DivOrder n by A75, ORDERS_2:def 5;

reconsider b9 = bb9 as bag of n ;

set N = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } ;

{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } in M by A74;

then reconsider N = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } as Element of M ;

take b9 ; :: thesis: ( b9 in HT (G,T) & b9 divides b )

consider r being Polynomial of n,L such that

r in I and

A77: N = {r} and

r <> 0_ (n,L) by A12;

r in N by A77, TARSKI:def 1;

then consider r9 being Polynomial of n,L such that

A78: r = r9 and

r9 in I and

A79: HM (r9,T) = Monom ((1. L),b9) and

A80: r9 <> 0_ (n,L) and

for q being Polynomial of n,L holds

( not q in I or not q < r9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ;

A81: r9 in G by A77, A78;

b9 = term (HM (r9,T)) by A79, POLYNOM7:10

.= HT (r9,T) by TERMORD:22 ;

hence ( b9 in HT (G,T) & b9 divides b ) by A76, A80, A81, Def5; :: thesis: verum

end;( b9 in HT (G,T) & b9 divides b ) )

reconsider bb = b as Element of RelStr(# (Bags n),(DivOrder n) #) by PRE_POLY:def 12;

assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

then consider bb9 being Element of RelStr(# (Bags n),(DivOrder n) #) such that

A74: bb9 in S and

A75: bb9 <= bb by A6, DICKSON:def 9;

A76: [bb9,bb] in DivOrder n by A75, ORDERS_2:def 5;

reconsider b9 = bb9 as bag of n ;

set N = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } ;

{ p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } in M by A74;

then reconsider N = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),b9) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ) ) } as Element of M ;

take b9 ; :: thesis: ( b9 in HT (G,T) & b9 divides b )

consider r being Polynomial of n,L such that

r in I and

A77: N = {r} and

r <> 0_ (n,L) by A12;

r in N by A77, TARSKI:def 1;

then consider r9 being Polynomial of n,L such that

A78: r = r9 and

r9 in I and

A79: HM (r9,T) = Monom ((1. L),b9) and

A80: r9 <> 0_ (n,L) and

for q being Polynomial of n,L holds

( not q in I or not q < r9,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),b9) ) ;

A81: r9 in G by A77, A78;

b9 = term (HM (r9,T)) by A79, POLYNOM7:10

.= HT (r9,T) by TERMORD:22 ;

hence ( b9 in HT (G,T) & b9 divides b ) by A76, A80, A81, Def5; :: thesis: verum

hence G is_Groebner_basis_of I,T by A45, Th29; :: thesis: G is_reduced_wrt T

now :: thesis: for q being Polynomial of n,L st q in G holds

( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )

hence
G is_reduced_wrt T
; :: thesis: verum( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )

let q be Polynomial of n,L; :: thesis: ( q in G implies ( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T ) )

assume A82: q in G ; :: thesis: ( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )

then consider rr being Polynomial of n,L such that

A83: q = rr and

A84: ex x being Element of M st x = {rr} ;

consider x being Element of M such that

A85: x = {rr} by A84;

x in M ;

then consider s being Element of Bags n such that

A86: x = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } and

A87: s in S ;

rr in x by A85, TARSKI:def 1;

then consider p being Polynomial of n,L such that

A88: rr = p and

p in I and

A89: HM (p,T) = Monom ((1. L),s) and

p <> 0_ (n,L) and

A90: for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) by A86;

A91: 1. L = coefficient (HM (rr,T)) by A88, A89, POLYNOM7:9

.= HC (rr,T) by TERMORD:22 ;

hence q is_monic_wrt T by A83; :: thesis: q is_irreducible_wrt G \ {q},T

A92: s = term (HM (rr,T)) by A88, A89, POLYNOM7:10

.= HT (q,T) by A83, TERMORD:22 ;

end;assume A82: q in G ; :: thesis: ( q is_monic_wrt T & q is_irreducible_wrt G \ {q},T )

then consider rr being Polynomial of n,L such that

A83: q = rr and

A84: ex x being Element of M st x = {rr} ;

consider x being Element of M such that

A85: x = {rr} by A84;

x in M ;

then consider s being Element of Bags n such that

A86: x = { p where p is Polynomial of n,L : ( p in I & HM (p,T) = Monom ((1. L),s) & p <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) ) ) } and

A87: s in S ;

rr in x by A85, TARSKI:def 1;

then consider p being Polynomial of n,L such that

A88: rr = p and

p in I and

A89: HM (p,T) = Monom ((1. L),s) and

p <> 0_ (n,L) and

A90: for q being Polynomial of n,L holds

( not q in I or not q < p,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),s) ) by A86;

A91: 1. L = coefficient (HM (rr,T)) by A88, A89, POLYNOM7:9

.= HC (rr,T) by TERMORD:22 ;

hence q is_monic_wrt T by A83; :: thesis: q is_irreducible_wrt G \ {q},T

A92: s = term (HM (rr,T)) by A88, A89, POLYNOM7:10

.= HT (q,T) by A83, TERMORD:22 ;

now :: thesis: ( q is_reducible_wrt G \ {q},T implies q is_irreducible_wrt G \ {q},T )

hence
q is_irreducible_wrt G \ {q},T
; :: thesis: verumreconsider htq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

assume q is_reducible_wrt G \ {q},T ; :: thesis: q is_irreducible_wrt G \ {q},T

then consider pp being Polynomial of n,L such that

A93: q reduces_to pp,G \ {q},T by POLYRED:def 9;

consider g being Polynomial of n,L such that

A94: g in G \ {q} and

A95: q reduces_to pp,g,T by A93, POLYRED:def 7;

A96: g in G by A94, XBOOLE_0:def 5;

A97: not g in {q} by A94, XBOOLE_0:def 5;

reconsider htg = HT (g,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

consider b being bag of n such that

A98: q reduces_to pp,g,b,T by A95, POLYRED:def 6;

A99: b in Support q by A98, POLYRED:def 5;

A100: ex s being bag of n st

( s + (HT (g,T)) = b & pp = q - (((q . b) / (HC (g,T))) * (s *' g)) ) by A98, POLYRED:def 5;

end;assume q is_reducible_wrt G \ {q},T ; :: thesis: q is_irreducible_wrt G \ {q},T

then consider pp being Polynomial of n,L such that

A93: q reduces_to pp,G \ {q},T by POLYRED:def 9;

consider g being Polynomial of n,L such that

A94: g in G \ {q} and

A95: q reduces_to pp,g,T by A93, POLYRED:def 7;

A96: g in G by A94, XBOOLE_0:def 5;

A97: not g in {q} by A94, XBOOLE_0:def 5;

reconsider htg = HT (g,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

consider b being bag of n such that

A98: q reduces_to pp,g,b,T by A95, POLYRED:def 6;

A99: b in Support q by A98, POLYRED:def 5;

A100: ex s being bag of n st

( s + (HT (g,T)) = b & pp = q - (((q . b) / (HC (g,T))) * (s *' g)) ) by A98, POLYRED:def 5;

now :: thesis: ( ( b = HT (q,T) & q is_irreducible_wrt G \ {q},T ) or ( b <> HT (q,T) & contradiction ) )end;

hence
q is_irreducible_wrt G \ {q},T
; :: thesis: verumper cases
( b = HT (q,T) or b <> HT (q,T) )
;

end;

case A101:
b = HT (q,T)
; :: thesis: q is_irreducible_wrt G \ {q},T

set S9 = S \ {htq};

consider z being Polynomial of n,L such that

A102: g = z and

A103: ex x being Element of M st x = {z} by A96;

consider x1 being Element of M such that

A104: x1 = {z} by A103;

x1 in M ;

then consider t being Element of Bags n such that

A105: x1 = { u where u is Polynomial of n,L : ( u in I & HM (u,T) = Monom ((1. L),t) & u <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < u,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),t) ) ) ) } and

A106: t in S ;

z in x1 by A104, TARSKI:def 1;

then consider p1 being Polynomial of n,L such that

A107: z = p1 and

p1 in I and

A108: HM (p1,T) = Monom ((1. L),t) and

p1 <> 0_ (n,L) and

for q being Polynomial of n,L holds

( not q in I or not q < p1,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),t) ) by A105;

A109: t = term (HM (p1,T)) by A108, POLYNOM7:10

.= htg by A102, A107, TERMORD:22 ;

HT (g,T) divides HT (q,T) by A100, A101, PRE_POLY:50;

then [htg,htq] in DivOrder n by Def5;

then A111: htg <= htq by ORDERS_2:def 5;

then S \ {htq} c= hti by A10;

then S \ {htq} is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) by A112, DICKSON:def 9;

then S c= S \ {htq} by A7;

hence q is_irreducible_wrt G \ {q},T by A87, A92, A115; :: thesis: verum

end;consider z being Polynomial of n,L such that

A102: g = z and

A103: ex x being Element of M st x = {z} by A96;

consider x1 being Element of M such that

A104: x1 = {z} by A103;

x1 in M ;

then consider t being Element of Bags n such that

A105: x1 = { u where u is Polynomial of n,L : ( u in I & HM (u,T) = Monom ((1. L),t) & u <> 0_ (n,L) & ( for q being Polynomial of n,L holds

( not q in I or not q < u,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),t) ) ) ) } and

A106: t in S ;

z in x1 by A104, TARSKI:def 1;

then consider p1 being Polynomial of n,L such that

A107: z = p1 and

p1 in I and

A108: HM (p1,T) = Monom ((1. L),t) and

p1 <> 0_ (n,L) and

for q being Polynomial of n,L holds

( not q in I or not q < p1,T or not q <> 0_ (n,L) or not HM (q,T) = Monom ((1. L),t) ) by A105;

A109: t = term (HM (p1,T)) by A108, POLYNOM7:10

.= htg by A102, A107, TERMORD:22 ;

now :: thesis: not htg in {htq}

then A110:
htg in S \ {htq}
by A106, A109, XBOOLE_0:def 5;assume
htg in {htq}
; :: thesis: contradiction

then t = s by A92, A109, TARSKI:def 1;

hence contradiction by A83, A85, A86, A97, A102, A104, A105, TARSKI:def 1; :: thesis: verum

end;then t = s by A92, A109, TARSKI:def 1;

hence contradiction by A83, A85, A86, A97, A102, A104, A105, TARSKI:def 1; :: thesis: verum

HT (g,T) divides HT (q,T) by A100, A101, PRE_POLY:50;

then [htg,htq] in DivOrder n by Def5;

then A111: htg <= htq by ORDERS_2:def 5;

A112: now :: thesis: for a being Element of RelStr(# (Bags n),(DivOrder n) #) st a in hti holds

ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a )

ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a )

let a be Element of RelStr(# (Bags n),(DivOrder n) #); :: thesis: ( a in hti implies ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) )

assume a in hti ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a )

then consider b being Element of RelStr(# (Bags n),(DivOrder n) #) such that

A113: b in S and

A114: b <= a by A6, DICKSON:def 9;

( b in S \ {htq} & b <= a ) ; :: thesis: verum

end;( b in S \ {htq} & b <= a ) )

assume a in hti ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a )

then consider b being Element of RelStr(# (Bags n),(DivOrder n) #) such that

A113: b in S and

A114: b <= a by A6, DICKSON:def 9;

now :: thesis: ( ( b in S \ {htq} & ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) ) or ( not b in S \ {htq} & ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) ) )end;

hence
ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st ( b in S \ {htq} & b <= a ) ) or ( not b in S \ {htq} & ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) ) )

per cases
( b in S \ {htq} or not b in S \ {htq} )
;

end;

case
b in S \ {htq}
; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a )

( b in S \ {htq} & b <= a )

hence
ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) by A114; :: thesis: verum

end;( b in S \ {htq} & b <= a ) by A114; :: thesis: verum

case
not b in S \ {htq}
; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a )

( b in S \ {htq} & b <= a )

then
b in {htq}
by A113, XBOOLE_0:def 5;

then htg <= b by A111, TARSKI:def 1;

hence ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) by A110, A114, ORDERS_2:3; :: thesis: verum

end;then htg <= b by A111, TARSKI:def 1;

hence ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S \ {htq} & b <= a ) by A110, A114, ORDERS_2:3; :: thesis: verum

( b in S \ {htq} & b <= a ) ; :: thesis: verum

A115: now :: thesis: not htq in S \ {htq}

S \ {htq} c= S
by XBOOLE_1:36;assume
htq in S \ {htq}
; :: thesis: contradiction

then not htq in {htq} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

end;then not htq in {htq} by XBOOLE_0:def 5;

hence contradiction by TARSKI:def 1; :: thesis: verum

then S \ {htq} c= hti by A10;

then S \ {htq} is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) by A112, DICKSON:def 9;

then S c= S \ {htq} by A7;

hence q is_irreducible_wrt G \ {q},T by A87, A92, A115; :: thesis: verum

case A116:
b <> HT (q,T)
; :: thesis: contradiction

b <= HT (q,T),T
by A99, TERMORD:def 6;

then b < HT (q,T),T by A116, TERMORD:def 3;

then A117: pp . (HT (q,T)) = q . (HT (q,T)) by A98, POLYRED:41

.= 1. L by A83, A91, TERMORD:def 7 ;

1. L <> 0. L ;

then A118: HT (q,T) in Support pp by A117, POLYNOM1:def 4;

HT (q,T) <= HT (pp,T),T by A118, TERMORD:def 6;

then HT (pp,T) = HT (q,T) by A121, TERMORD:7;

then Monom ((HC (pp,T)),(HT (pp,T))) = Monom ((1. L),s) by A92, A117, TERMORD:def 7;

then A122: HM (pp,T) = HM (q,T) by A83, A88, A89, TERMORD:def 8;

A124: pp = q - (m *' g) by A95, Th1;

reconsider gg = g, qq = q, mm = m as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider gg = gg, qq = qq, mm = mm as Element of (Polynom-Ring (n,L)) ;

g in G by A94, XBOOLE_0:def 5;

then mm * gg in I by A45, IDEAL_1:def 2;

then - (mm * gg) in I by IDEAL_1:13;

then A125: qq + (- (mm * gg)) in I by A45, A82, IDEAL_1:def 1;

mm * gg = m *' g by POLYNOM1:def 11;

then q - (m *' g) = qq - (mm * gg) by Lm2;

then pp in I by A124, A125;

hence contradiction by A83, A88, A89, A90, A95, A122, A123, POLYRED:43; :: thesis: verum

end;then b < HT (q,T),T by A116, TERMORD:def 3;

then A117: pp . (HT (q,T)) = q . (HT (q,T)) by A98, POLYRED:41

.= 1. L by A83, A91, TERMORD:def 7 ;

1. L <> 0. L ;

then A118: HT (q,T) in Support pp by A117, POLYNOM1:def 4;

now :: thesis: not HT (q,T) < HT (pp,T),T

then A121:
HT (pp,T) <= HT (q,T),T
by TERMORD:5;A119:
b <= HT (q,T),T
by A99, TERMORD:def 6;

assume A120: HT (q,T) < HT (pp,T),T ; :: thesis: contradiction

then HT (q,T) <= HT (pp,T),T by TERMORD:def 3;

then ( b <= HT (pp,T),T & b <> HT (pp,T) ) by A116, A119, TERMORD:7, TERMORD:8;

then b < HT (pp,T),T by TERMORD:def 3;

then ( HT (pp,T) in Support q iff HT (pp,T) in Support pp ) by A98, POLYRED:40;

then HT (pp,T) <= HT (q,T),T by A118, TERMORD:def 6;

hence contradiction by A120, TERMORD:5; :: thesis: verum

end;assume A120: HT (q,T) < HT (pp,T),T ; :: thesis: contradiction

then HT (q,T) <= HT (pp,T),T by TERMORD:def 3;

then ( b <= HT (pp,T),T & b <> HT (pp,T) ) by A116, A119, TERMORD:7, TERMORD:8;

then b < HT (pp,T),T by TERMORD:def 3;

then ( HT (pp,T) in Support q iff HT (pp,T) in Support pp ) by A98, POLYRED:40;

then HT (pp,T) <= HT (q,T),T by A118, TERMORD:def 6;

hence contradiction by A120, TERMORD:5; :: thesis: verum

HT (q,T) <= HT (pp,T),T by A118, TERMORD:def 6;

then HT (pp,T) = HT (q,T) by A121, TERMORD:7;

then Monom ((HC (pp,T)),(HT (pp,T))) = Monom ((1. L),s) by A92, A117, TERMORD:def 7;

then A122: HM (pp,T) = HM (q,T) by A83, A88, A89, TERMORD:def 8;

A123: now :: thesis: not pp = 0_ (n,L)

consider m being Monomial of n,L such that assume
pp = 0_ (n,L)
; :: thesis: contradiction

then 0. L = HC (pp,T) by TERMORD:17

.= coefficient (HM (pp,T)) by TERMORD:22

.= 1. L by A83, A91, A122, TERMORD:22 ;

hence contradiction ; :: thesis: verum

end;then 0. L = HC (pp,T) by TERMORD:17

.= coefficient (HM (pp,T)) by TERMORD:22

.= 1. L by A83, A91, A122, TERMORD:22 ;

hence contradiction ; :: thesis: verum

A124: pp = q - (m *' g) by A95, Th1;

reconsider gg = g, qq = q, mm = m as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;

reconsider gg = gg, qq = qq, mm = mm as Element of (Polynom-Ring (n,L)) ;

g in G by A94, XBOOLE_0:def 5;

then mm * gg in I by A45, IDEAL_1:def 2;

then - (mm * gg) in I by IDEAL_1:13;

then A125: qq + (- (mm * gg)) in I by A45, A82, IDEAL_1:def 1;

mm * gg = m *' g by POLYNOM1:def 11;

then q - (m *' g) = qq - (mm * gg) by Lm2;

then pp in I by A124, A125;

hence contradiction by A83, A88, A89, A90, A95, A122, A123, POLYRED:43; :: thesis: verum