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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_wrt T

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) implies G is_Groebner_basis_wrt T )

assume A1: not 0_ (n,L) in G ; :: thesis: ( ex g1, g2 being Polynomial of n,L st

( g1 in G & g2 in G & not PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) or G is_Groebner_basis_wrt T )

assume A2: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ; :: thesis: G is_Groebner_basis_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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) holds

G is_Groebner_basis_wrt T

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) implies G is_Groebner_basis_wrt T )

assume A1: not 0_ (n,L) in G ; :: thesis: ( ex g1, g2 being Polynomial of n,L st

( g1 in G & g2 in G & not PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ) or G is_Groebner_basis_wrt T )

assume A2: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) ; :: thesis: G is_Groebner_basis_wrt T

now :: thesis: for g1, g2 being Polynomial of n,L st g1 <> g2 & g1 in G & g2 in G holds

for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

hence
G is_Groebner_basis_wrt T
by Th17; :: thesis: verumfor m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

let g1, g2 be Polynomial of n,L; :: thesis: ( g1 <> g2 & g1 in G & g2 in G implies for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) )

assume that

g1 <> g2 and

A3: g1 in G and

A4: g2 in G ; :: thesis: for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

thus for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) :: thesis: verum

end;PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) )

assume that

g1 <> g2 and

A3: g1 in G and

A4: g2 in G ; :: thesis: for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

thus for m1, m2 being Monomial of n,L st HM ((m1 *' g1),T) = HM ((m2 *' g2),T) holds

PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) :: thesis: verum

proof

set a1 = HC (g1,T);

set a2 = HC (g2,T);

set t1 = HT (g1,T);

set t2 = HT (g2,T);

let m1, m2 be Monomial of n,L; :: thesis: ( HM ((m1 *' g1),T) = HM ((m2 *' g2),T) implies PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) )

assume A5: HM ((m1 *' g1),T) = HM ((m2 *' g2),T) ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

A6: HC (g2,T) <> 0. L by A1, A4, TERMORD:17;

reconsider g1 = g1, g2 = g2 as non-zero Polynomial of n,L by A1, A3, A4, POLYNOM7:def 1;

set b1 = coefficient m1;

set b2 = coefficient m2;

set u1 = term m1;

set u2 = term m2;

A7: HC (g1,T) <> 0. L by A1, A3, TERMORD:17;

then reconsider a1 = HC (g1,T), a2 = HC (g2,T) as non zero Element of L by A6, STRUCT_0:def 12;

A8: HC ((m1 *' g1),T) = coefficient (HM ((m1 *' g1),T)) by TERMORD:22

.= HC ((m2 *' g2),T) by A5, TERMORD:22 ;

end;set a2 = HC (g2,T);

set t1 = HT (g1,T);

set t2 = HT (g2,T);

let m1, m2 be Monomial of n,L; :: thesis: ( HM ((m1 *' g1),T) = HM ((m2 *' g2),T) implies PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) )

assume A5: HM ((m1 *' g1),T) = HM ((m2 *' g2),T) ; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

A6: HC (g2,T) <> 0. L by A1, A4, TERMORD:17;

reconsider g1 = g1, g2 = g2 as non-zero Polynomial of n,L by A1, A3, A4, POLYNOM7:def 1;

set b1 = coefficient m1;

set b2 = coefficient m2;

set u1 = term m1;

set u2 = term m2;

A7: HC (g1,T) <> 0. L by A1, A3, TERMORD:17;

then reconsider a1 = HC (g1,T), a2 = HC (g2,T) as non zero Element of L by A6, STRUCT_0:def 12;

A8: HC ((m1 *' g1),T) = coefficient (HM ((m1 *' g1),T)) by TERMORD:22

.= HC ((m2 *' g2),T) by A5, TERMORD:22 ;

now :: thesis: ( ( ( coefficient m1 = 0. L or coefficient m2 = 0. L ) & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) or ( coefficient m1 <> 0. L & coefficient m2 <> 0. L & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) )end;

hence
PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)
; :: thesis: verumper cases
( coefficient m1 = 0. L or coefficient m2 = 0. L or ( coefficient m1 <> 0. L & coefficient m2 <> 0. L ) )
;

end;

case A9:
( coefficient m1 = 0. L or coefficient m2 = 0. L )
; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

end;

now :: thesis: ( ( coefficient m1 = 0. L & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) or ( coefficient m2 = 0. L & PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) ) )end;

hence
PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)
; :: thesis: verumper cases
( coefficient m1 = 0. L or coefficient m2 = 0. L )
by A9;

end;

case
coefficient m1 = 0. L
; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

then
HC (m1,T) = 0. L
by TERMORD:23;

then m1 = 0_ (n,L) by TERMORD:17;

then A10: m1 *' g1 = 0_ (n,L) by POLYRED:5;

then HC ((m2 *' g2),T) = 0. L by A8, TERMORD:17;

then m2 *' g2 = 0_ (n,L) by TERMORD:17;

then (m1 *' g1) - (m2 *' g2) = 0_ (n,L) by A10, POLYRED:4;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by REWRITE1:12; :: thesis: verum

end;then m1 = 0_ (n,L) by TERMORD:17;

then A10: m1 *' g1 = 0_ (n,L) by POLYRED:5;

then HC ((m2 *' g2),T) = 0. L by A8, TERMORD:17;

then m2 *' g2 = 0_ (n,L) by TERMORD:17;

then (m1 *' g1) - (m2 *' g2) = 0_ (n,L) by A10, POLYRED:4;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by REWRITE1:12; :: thesis: verum

case
coefficient m2 = 0. L
; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

then
HC (m2,T) = 0. L
by TERMORD:23;

then m2 = 0_ (n,L) by TERMORD:17;

then A11: m2 *' g2 = 0_ (n,L) by POLYRED:5;

then HC ((m1 *' g1),T) = 0. L by A8, TERMORD:17;

then m1 *' g1 = 0_ (n,L) by TERMORD:17;

then (m1 *' g1) - (m2 *' g2) = 0_ (n,L) by A11, POLYRED:4;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by REWRITE1:12; :: thesis: verum

end;then m2 = 0_ (n,L) by TERMORD:17;

then A11: m2 *' g2 = 0_ (n,L) by POLYRED:5;

then HC ((m1 *' g1),T) = 0. L by A8, TERMORD:17;

then m1 *' g1 = 0_ (n,L) by TERMORD:17;

then (m1 *' g1) - (m2 *' g2) = 0_ (n,L) by A11, POLYRED:4;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by REWRITE1:12; :: thesis: verum

case A12:
( coefficient m1 <> 0. L & coefficient m2 <> 0. L )
; :: thesis: PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L)

then reconsider b1 = coefficient m1, b2 = coefficient m2 as non zero Element of L by STRUCT_0:def 12;

b2 * a2 <> 0. L by VECTSP_2:def 1;

then A13: not b2 * a2 is zero ;

HT (g1,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then consider s1 being bag of n such that

A14: (HT (g1,T)) + s1 = lcm ((HT (g1,T)),(HT (g2,T))) by TERMORD:1;

HC (m2,T) <> 0. L by A12, TERMORD:23;

then A15: m2 <> 0_ (n,L) by TERMORD:17;

HC (m1,T) <> 0. L by A12, TERMORD:23;

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

then reconsider m1 = m1, m2 = m2 as non-zero Monomial of n,L by A15, POLYNOM7:def 1;

A16: Monom ((b1 * a1),((term m1) + (HT (g1,T)))) = (Monom (b1,(term m1))) *' (Monom (a1,(HT (g1,T)))) by TERMORD:3

.= m1 *' (Monom (a1,(HT (g1,T)))) by POLYNOM7:11

.= (HM (m1,T)) *' (Monom (a1,(HT (g1,T)))) by TERMORD:23

.= (HM (m1,T)) *' (HM (g1,T)) by TERMORD:def 8

.= HM ((m2 *' g2),T) by A5, TERMORD:33

.= (HM (m2,T)) *' (HM (g2,T)) by TERMORD:33

.= (HM (m2,T)) *' (Monom (a2,(HT (g2,T)))) by TERMORD:def 8

.= m2 *' (Monom (a2,(HT (g2,T)))) by TERMORD:23

.= (Monom (b2,(term m2))) *' (Monom (a2,(HT (g2,T)))) by POLYNOM7:11

.= Monom ((b2 * a2),((term m2) + (HT (g2,T)))) by TERMORD:3 ;

then b1 * a1 = coefficient (Monom ((b2 * a2),((term m2) + (HT (g2,T))))) by POLYNOM7:9

.= b2 * a2 by POLYNOM7:9 ;

then (b1 * a1) / a2 = (b2 * a2) * (a2 ")

.= b2 * (a2 * (a2 ")) by GROUP_1:def 3

.= b2 * (1. L) by A6, VECTSP_1:def 10 ;

then A17: b2 / a1 = ((b1 * a1) / a2) / a1

.= ((b1 * a1) * (a2 ")) / a1

.= ((b1 * a1) * (a2 ")) * (a1 ")

.= ((b1 * (a2 ")) * a1) * (a1 ") by GROUP_1:def 3

.= (b1 * (a2 ")) * (a1 * (a1 ")) by GROUP_1:def 3

.= (b1 * (a2 ")) * (1. L) by A7, VECTSP_1:def 10

.= b1 * (a2 ")

.= b1 / a2 ;

b1 * a1 <> 0. L by VECTSP_2:def 1;

then not b1 * a1 is zero ;

then A18: (term m1) + (HT (g1,T)) = term (Monom ((b2 * a2),((term m2) + (HT (g2,T))))) by A16, POLYNOM7:10

.= (term m2) + (HT (g2,T)) by A13, POLYNOM7:10 ;

then ( HT (g1,T) divides (term m1) + (HT (g1,T)) & HT (g2,T) divides (term m1) + (HT (g1,T)) ) by TERMORD:1;

then lcm ((HT (g1,T)),(HT (g2,T))) divides (term m1) + (HT (g1,T)) by Th4;

then consider v being bag of n such that

A19: (term m1) + (HT (g1,T)) = (lcm ((HT (g1,T)),(HT (g2,T)))) + v by TERMORD:1;

(term m1) + (HT (g1,T)) = (v + s1) + (HT (g1,T)) by A14, A19, PRE_POLY:35;

then A20: term m1 = ((v + s1) + (HT (g1,T))) -' (HT (g1,T)) by PRE_POLY:48

.= v + s1 by PRE_POLY:48 ;

HT (g2,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then consider s2 being bag of n such that

A21: (HT (g2,T)) + s2 = lcm ((HT (g1,T)),(HT (g2,T))) by TERMORD:1;

(term m2) + (HT (g2,T)) = (v + s2) + (HT (g2,T)) by A18, A21, A19, PRE_POLY:35;

then A22: term m2 = ((v + s2) + (HT (g2,T))) -' (HT (g2,T)) by PRE_POLY:48

.= v + s2 by PRE_POLY:48 ;

HT (g2,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then A23: s2 = (lcm ((HT (g1,T)),(HT (g2,T)))) / (HT (g2,T)) by A21, Def1;

A24: (b2 / a1) * a1 = (b2 * (a1 ")) * a1

.= b2 * ((a1 ") * a1) by GROUP_1:def 3

.= b2 * (1. L) by A7, VECTSP_1:def 10

.= b2 ;

HT (g1,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then A25: s1 = (lcm ((HT (g1,T)),(HT (g2,T)))) / (HT (g1,T)) by A14, Def1;

A26: (b1 / a2) * a2 = (b1 * (a2 ")) * a2

.= b1 * ((a2 ") * a2) by GROUP_1:def 3

.= b1 * (1. L) by A6, VECTSP_1:def 10 ;

(m1 *' g1) - (m2 *' g2) = ((Monom (b1,(term m1))) *' g1) - (m2 *' g2) by POLYNOM7:11

.= ((Monom (b1,(term m1))) *' g1) - ((Monom (b2,(term m2))) *' g2) by POLYNOM7:11

.= (b1 * ((v + s1) *' g1)) - ((Monom (b2,(v + s2))) *' g2) by A20, A22, POLYRED:22

.= (b1 * (v *' (s1 *' g1))) - ((Monom (b2,(v + s2))) *' g2) by POLYRED:18

.= (b1 * (v *' (s1 *' g1))) - (b2 * ((v + s2) *' g2)) by POLYRED:22

.= (b1 * (v *' (s1 *' g1))) - (b2 * (v *' (s2 *' g2))) by POLYRED:18

.= (b1 * (v *' (s1 *' g1))) + (- (b2 * (v *' (s2 *' g2)))) by POLYNOM1:def 7

.= (b1 * (v *' (s1 *' g1))) + (b2 * (- (v *' (s2 *' g2)))) by POLYRED:9

.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (- (v *' (s2 *' g2)))) by A26, A24

.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (v *' (- (s2 *' g2)))) by Th13

.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2))))) by A17, POLYRED:11

.= ((b1 / a2) * (a2 * (v *' (s1 *' g1)))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2))))) by POLYRED:11

.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (a1 * (v *' (- (s2 *' g2))))) by Th15

.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (a1 * (- (s2 *' g2))))) by Th14

.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2))))) by POLYRED:9

.= (b1 / a2) * ((v *' (a2 * (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2))))) by Th14

.= (b1 / a2) * (v *' ((a2 * (s1 *' g1)) + (- (a1 * (s2 *' g2))))) by Th12

.= (b1 / a2) * (v *' (S-Poly (g1,g2,T))) by A25, A23, POLYNOM1:def 7

.= (Monom ((b1 / a2),v)) *' (S-Poly (g1,g2,T)) by POLYRED:22 ;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by A2, A3, A4, POLYRED:48; :: thesis: verum

end;b2 * a2 <> 0. L by VECTSP_2:def 1;

then A13: not b2 * a2 is zero ;

HT (g1,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then consider s1 being bag of n such that

A14: (HT (g1,T)) + s1 = lcm ((HT (g1,T)),(HT (g2,T))) by TERMORD:1;

HC (m2,T) <> 0. L by A12, TERMORD:23;

then A15: m2 <> 0_ (n,L) by TERMORD:17;

HC (m1,T) <> 0. L by A12, TERMORD:23;

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

then reconsider m1 = m1, m2 = m2 as non-zero Monomial of n,L by A15, POLYNOM7:def 1;

A16: Monom ((b1 * a1),((term m1) + (HT (g1,T)))) = (Monom (b1,(term m1))) *' (Monom (a1,(HT (g1,T)))) by TERMORD:3

.= m1 *' (Monom (a1,(HT (g1,T)))) by POLYNOM7:11

.= (HM (m1,T)) *' (Monom (a1,(HT (g1,T)))) by TERMORD:23

.= (HM (m1,T)) *' (HM (g1,T)) by TERMORD:def 8

.= HM ((m2 *' g2),T) by A5, TERMORD:33

.= (HM (m2,T)) *' (HM (g2,T)) by TERMORD:33

.= (HM (m2,T)) *' (Monom (a2,(HT (g2,T)))) by TERMORD:def 8

.= m2 *' (Monom (a2,(HT (g2,T)))) by TERMORD:23

.= (Monom (b2,(term m2))) *' (Monom (a2,(HT (g2,T)))) by POLYNOM7:11

.= Monom ((b2 * a2),((term m2) + (HT (g2,T)))) by TERMORD:3 ;

then b1 * a1 = coefficient (Monom ((b2 * a2),((term m2) + (HT (g2,T))))) by POLYNOM7:9

.= b2 * a2 by POLYNOM7:9 ;

then (b1 * a1) / a2 = (b2 * a2) * (a2 ")

.= b2 * (a2 * (a2 ")) by GROUP_1:def 3

.= b2 * (1. L) by A6, VECTSP_1:def 10 ;

then A17: b2 / a1 = ((b1 * a1) / a2) / a1

.= ((b1 * a1) * (a2 ")) / a1

.= ((b1 * a1) * (a2 ")) * (a1 ")

.= ((b1 * (a2 ")) * a1) * (a1 ") by GROUP_1:def 3

.= (b1 * (a2 ")) * (a1 * (a1 ")) by GROUP_1:def 3

.= (b1 * (a2 ")) * (1. L) by A7, VECTSP_1:def 10

.= b1 * (a2 ")

.= b1 / a2 ;

b1 * a1 <> 0. L by VECTSP_2:def 1;

then not b1 * a1 is zero ;

then A18: (term m1) + (HT (g1,T)) = term (Monom ((b2 * a2),((term m2) + (HT (g2,T))))) by A16, POLYNOM7:10

.= (term m2) + (HT (g2,T)) by A13, POLYNOM7:10 ;

then ( HT (g1,T) divides (term m1) + (HT (g1,T)) & HT (g2,T) divides (term m1) + (HT (g1,T)) ) by TERMORD:1;

then lcm ((HT (g1,T)),(HT (g2,T))) divides (term m1) + (HT (g1,T)) by Th4;

then consider v being bag of n such that

A19: (term m1) + (HT (g1,T)) = (lcm ((HT (g1,T)),(HT (g2,T)))) + v by TERMORD:1;

(term m1) + (HT (g1,T)) = (v + s1) + (HT (g1,T)) by A14, A19, PRE_POLY:35;

then A20: term m1 = ((v + s1) + (HT (g1,T))) -' (HT (g1,T)) by PRE_POLY:48

.= v + s1 by PRE_POLY:48 ;

HT (g2,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then consider s2 being bag of n such that

A21: (HT (g2,T)) + s2 = lcm ((HT (g1,T)),(HT (g2,T))) by TERMORD:1;

(term m2) + (HT (g2,T)) = (v + s2) + (HT (g2,T)) by A18, A21, A19, PRE_POLY:35;

then A22: term m2 = ((v + s2) + (HT (g2,T))) -' (HT (g2,T)) by PRE_POLY:48

.= v + s2 by PRE_POLY:48 ;

HT (g2,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then A23: s2 = (lcm ((HT (g1,T)),(HT (g2,T)))) / (HT (g2,T)) by A21, Def1;

A24: (b2 / a1) * a1 = (b2 * (a1 ")) * a1

.= b2 * ((a1 ") * a1) by GROUP_1:def 3

.= b2 * (1. L) by A7, VECTSP_1:def 10

.= b2 ;

HT (g1,T) divides lcm ((HT (g1,T)),(HT (g2,T))) by Th3;

then A25: s1 = (lcm ((HT (g1,T)),(HT (g2,T)))) / (HT (g1,T)) by A14, Def1;

A26: (b1 / a2) * a2 = (b1 * (a2 ")) * a2

.= b1 * ((a2 ") * a2) by GROUP_1:def 3

.= b1 * (1. L) by A6, VECTSP_1:def 10 ;

(m1 *' g1) - (m2 *' g2) = ((Monom (b1,(term m1))) *' g1) - (m2 *' g2) by POLYNOM7:11

.= ((Monom (b1,(term m1))) *' g1) - ((Monom (b2,(term m2))) *' g2) by POLYNOM7:11

.= (b1 * ((v + s1) *' g1)) - ((Monom (b2,(v + s2))) *' g2) by A20, A22, POLYRED:22

.= (b1 * (v *' (s1 *' g1))) - ((Monom (b2,(v + s2))) *' g2) by POLYRED:18

.= (b1 * (v *' (s1 *' g1))) - (b2 * ((v + s2) *' g2)) by POLYRED:22

.= (b1 * (v *' (s1 *' g1))) - (b2 * (v *' (s2 *' g2))) by POLYRED:18

.= (b1 * (v *' (s1 *' g1))) + (- (b2 * (v *' (s2 *' g2)))) by POLYNOM1:def 7

.= (b1 * (v *' (s1 *' g1))) + (b2 * (- (v *' (s2 *' g2)))) by POLYRED:9

.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (- (v *' (s2 *' g2)))) by A26, A24

.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + (((b2 / a1) * a1) * (v *' (- (s2 *' g2)))) by Th13

.= (((b1 / a2) * a2) * (v *' (s1 *' g1))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2))))) by A17, POLYRED:11

.= ((b1 / a2) * (a2 * (v *' (s1 *' g1)))) + ((b1 / a2) * (a1 * (v *' (- (s2 *' g2))))) by POLYRED:11

.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (a1 * (v *' (- (s2 *' g2))))) by Th15

.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (a1 * (- (s2 *' g2))))) by Th14

.= (b1 / a2) * ((a2 * (v *' (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2))))) by POLYRED:9

.= (b1 / a2) * ((v *' (a2 * (s1 *' g1))) + (v *' (- (a1 * (s2 *' g2))))) by Th14

.= (b1 / a2) * (v *' ((a2 * (s1 *' g1)) + (- (a1 * (s2 *' g2))))) by Th12

.= (b1 / a2) * (v *' (S-Poly (g1,g2,T))) by A25, A23, POLYNOM1:def 7

.= (Monom ((b1 / a2),v)) *' (S-Poly (g1,g2,T)) by POLYRED:22 ;

hence PolyRedRel (G,T) reduces (m1 *' g1) - (m2 *' g2), 0_ (n,L) by A2, A3, A4, POLYRED:48; :: thesis: verum