let n be Nat; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed left_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, h being Polynomial of n,L st f in P holds
PolyRedRel P,T reduces h *' f, 0_ n,L
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed left_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring n,L)
for f, h being Polynomial of n,L st f in P holds
PolyRedRel P,T reduces h *' f, 0_ n,L
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed left_zeroed doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring n,L)
for f, h being Polynomial of n,L st f in P holds
PolyRedRel P,T reduces h *' f, 0_ n,L
let P be Subset of (Polynom-Ring n,L); :: thesis: for f, h being Polynomial of n,L st f in P holds
PolyRedRel P,T reduces h *' f, 0_ n,L
let f', h' be Polynomial of n,L; :: thesis: ( f' in P implies PolyRedRel P,T reduces h' *' f', 0_ n,L )
assume A1: f' in P ; :: thesis: PolyRedRel P,T reduces h' *' f', 0_ n,L

per cases ( h' = 0_ n,L or h' <> 0_ n,L ) ;

suppose h' = 0_ n,L ; :: thesis: PolyRedRel P,T reduces h' *' f', 0_ n,L

then h' *' f' = 0_ n,L by Th5;
hence PolyRedRel P,T reduces h' *' f', 0_ n,L by REWRITE1:13; :: thesis: verum

end;

suppose h' <> 0_ n,L ; :: thesis: PolyRedRel P,T reduces h' *' f', 0_ n,L

then reconsider h = h' as non-zero Polynomial of n,L by POLYNOM7:def 2;
set H = { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f', 0_ n,L } ;

now

per cases ( f' = 0_ n,L or f' <> 0_ n,L ) ;

case f' = 0_ n,L ; :: thesis: PolyRedRel P,T reduces h' *' f', 0_ n,L

then h' *' f' = 0_ n,L by POLYNOM1:87;
hence PolyRedRel P,T reduces h' *' f', 0_ n,L by REWRITE1:13; :: thesis: verum

end;

case f' <> 0_ n,L ; :: thesis: ( not PolyRedRel P,T reduces h' *' f', 0_ n,L implies PolyRedRel P,T reduces h' *' f', 0_ n,L )

then reconsider f = f' as non-zero Polynomial of n,L by POLYNOM7:def 2;
assume not PolyRedRel P,T reduces h' *' f', 0_ n,L ; :: thesis: PolyRedRel P,T reduces h' *' f', 0_ n,L
then A2: h in { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f', 0_ n,L } ;

now

let u be set ; :: thesis: ( u in { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f', 0_ n,L } implies u in the carrier of (Polynom-Ring n,L) )
assume u in { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f', 0_ n,L } ; :: thesis: u in the carrier of (Polynom-Ring n,L)
then consider g' being Polynomial of n,L such that
A3: ( u = g' & not PolyRedRel P,T reduces g' *' f, 0_ n,L ) ;
thus u in the carrier of (Polynom-Ring n,L) by A3, POLYNOM1:def 27; :: thesis: verum

end;

then reconsider H = { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f', 0_ n,L } as non empty Subset of (Polynom-Ring n,L) by A2, TARSKI:def 3;

now

assume H <> {} ; :: thesis: contradiction
reconsider H = H as non empty set ;
consider m being Polynomial of n,L such that
A4: ( m in H & ( for m' being Polynomial of n,L st m' in H holds
m <= m',T ) ) by Th31;
m <> 0_ n,L

proof

assume A5: m = 0_ n,L ; :: thesis: contradiction
consider g' being Polynomial of n,L such that
A6: ( m = g' & not PolyRedRel P,T reduces g' *' f, 0_ n,L ) by A4;
m *' f = 0_ n,L by A5, Th5;
hence contradiction by A6, REWRITE1:13; :: thesis: verum

end;

then reconsider m = m as non-zero Polynomial of n,L by POLYNOM7:def 2;
A7: HT (m *' f),T = (HT m,T) + (HT f,T) by TERMORD:31;
m *' f <> 0_ n,L by POLYNOM7:def 2;
then Support (m *' f) <> {} by POLYNOM7:1;
then A8: HT (m *' f),T in Support (m *' f) by TERMORD:def 6;
set g = (m *' f) - ((((m *' f) . (HT (m *' f),T)) / (HC f,T)) * ((HT m,T) *' f));
( f <> 0_ n,L & m *' f <> 0_ n,L ) by POLYNOM7:def 2;
then A9: m *' f reduces_to (m *' f) - ((((m *' f) . (HT (m *' f),T)) / (HC f,T)) * ((HT m,T) *' f)),f, HT (m *' f),T,T by A7, A8, Def5;
f <> 0_ n,L by POLYNOM7:def 2;
then A10: HC f,T <> 0. L by TERMORD:17;
(((m *' f) . (HT (m *' f),T)) / (HC f,T)) * ((HT m,T) *' f) = ((HC (m *' f),T) / (HC f,T)) * ((HT m,T) *' f) by TERMORD:def 7
.= (((HC m,T) * (HC f,T)) / (HC f,T)) * ((HT m,T) *' f) by TERMORD:32
.= (((HC m,T) * (HC f,T)) * ((HC f,T) " )) * ((HT m,T) *' f) by VECTSP_1:def 23
.= ((HC m,T) * ((HC f,T) * ((HC f,T) " ))) * ((HT m,T) *' f) by GROUP_1:def 4
.= ((HC m,T) * (1. L)) * ((HT m,T) *' f) by A10, VECTSP_1:def 22
.= (HC m,T) * ((HT m,T) *' f) by VECTSP_1:def 13
.= (Monom (HC m,T),(HT m,T)) *' f by Th22
.= (HM m,T) *' f by TERMORD:def 8 ;
then (m *' f) - ((((m *' f) . (HT (m *' f),T)) / (HC f,T)) * ((HT m,T) *' f)) = (m *' f) + (- ((HM m,T) *' f)) by POLYNOM1:def 23
.= (f *' m) + (f *' (- (HM m,T))) by Th6
.= (m + (- (HM m,T))) *' f by POLYNOM1:85
.= (m - (HM m,T)) *' f by POLYNOM1:def 23
.= (Red m,T) *' f by TERMORD:def 9 ;
then m *' f reduces_to (Red m,T) *' f,f,T by A9, Def6;
then m *' f reduces_to (Red m,T) *' f,P,T by A1, Def7;
then [(m *' f),((Red m,T) *' f)] in PolyRedRel P,T by Def13;
then A11: PolyRedRel P,T reduces m *' f,(Red m,T) *' f by REWRITE1:16;
Red m,T < m,T by Th35;
then not m <= Red m,T,T by Th29;
then not Red m,T in H by A4;
then A12: PolyRedRel P,T reduces (Red m,T) *' f, 0_ n,L ;
consider u being Polynomial of n,L such that
A13: ( m = u & not PolyRedRel P,T reduces u *' f, 0_ n,L ) by A4;
thus contradiction by A11, A12, A13, REWRITE1:17; :: thesis: verum

end;

hence PolyRedRel P,T reduces h' *' f', 0_ n,L ; :: thesis: verum

end;

end;

end;

hence PolyRedRel P,T reduces h' *' f', 0_ n,L ; :: thesis: verum

end;

end;