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 f9, h9 be Polynomial of n,L; :: thesis: ( f9 in P implies PolyRedRel P,T reduces h9 *' f9, 0_ n,L )
assume A1: f9 in P ; :: thesis: PolyRedRel P,T reduces h9 *' f9, 0_ n,L

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

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

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

end;

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

then reconsider h = h9 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 *' f9, 0_ n,L } ;

now

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

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

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

end;

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

then reconsider f = f9 as non-zero Polynomial of n,L by POLYNOM7:def 2;

A2: now

let u be set ; :: thesis: ( u in { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f9, 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 *' f9, 0_ n,L } ; :: thesis: u in the carrier of (Polynom-Ring n,L)
then ex g9 being Polynomial of n,L st
( u = g9 & not PolyRedRel P,T reduces g9 *' f, 0_ n,L ) ;
hence u in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27; :: thesis: verum

end;

assume not PolyRedRel P,T reduces h9 *' f9, 0_ n,L ; :: thesis: PolyRedRel P,T reduces h9 *' f9, 0_ n,L
then h in { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f9, 0_ n,L } ;
then reconsider H = { g where g is Polynomial of n,L : not PolyRedRel P,T reduces g *' f9, 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
A3: m in H and
A4: for m9 being Polynomial of n,L st m9 in H holds
m <= m9,T by Th31;
m <> 0_ n,L

proof

assume m = 0_ n,L ; :: thesis: contradiction
then A5: m *' f = 0_ n,L by Th5;
ex g9 being Polynomial of n,L st
( m = g9 & not PolyRedRel P,T reduces g9 *' f, 0_ n,L ) by A3;
hence contradiction by A5, REWRITE1:13; :: thesis: verum

end;

then reconsider m = m as non-zero Polynomial of n,L by POLYNOM7:def 2;
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 A6: PolyRedRel P,T reduces (Red m,T) *' f, 0_ n,L ;
set g = (m *' f) - ((((m *' f) . (HT (m *' f),T)) / (HC f,T)) * ((HT m,T) *' f));
A7: m *' f <> 0_ n,L by POLYNOM7:def 2;
f <> 0_ n,L by POLYNOM7:def 2;
then A8: HC f,T <> 0. L by TERMORD:17;
m *' f <> 0_ n,L by POLYNOM7:def 2;
then Support (m *' f) <> {} by POLYNOM7:1;
then A9: HT (m *' f),T in Support (m *' f) by TERMORD:def 6;
(((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 A8, 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 A10: (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 ;
( HT (m *' f),T = (HT m,T) + (HT f,T) & f <> 0_ n,L ) by POLYNOM7:def 2, TERMORD:31;
then 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 A9, A7, Def5;
then m *' f reduces_to (Red m,T) *' f,f,T by A10, 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;
ex u being Polynomial of n,L st
( m = u & not PolyRedRel P,T reduces u *' f, 0_ n,L ) by A3;
hence contradiction by A11, A6, REWRITE1:17; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;