let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for P being Subset of (Polynom-Ring (n,L))
for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
let P be Subset of (Polynom-Ring (n,L)); :: thesis: for f being non-zero Polynomial of n,L
for g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
let f be non-zero Polynomial of n,L; :: thesis: for g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
let g be Polynomial of n,L; :: thesis: for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 & f reduces_to g,P,T holds
f9,g9 are_congruent_mod P -Ideal
let f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis: ( f = f9 & g = g9 & f reduces_to g,P,T implies f9,g9 are_congruent_mod P -Ideal )
assume that
A1: f = f9 and
A2: g = g9 ; :: thesis: ( not f reduces_to g,P,T or f9,g9 are_congruent_mod P -Ideal )
set R = Polynom-Ring (n,L);
reconsider x = - g as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider x = x as Element of (Polynom-Ring (n,L)) ;
x + g9 = (- g) + g by A2, POLYNOM1:def 11
.= 0_ (n,L) by Th3
.= 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11 ;
then A3: - g9 = - g by RLVECT_1:6;
assume f reduces_to g,P,T ; :: thesis: f9,g9 are_congruent_mod P -Ideal
then consider p being Polynomial of n,L such that
A4: p in P and
A5: f reduces_to g,p,T ;
consider b being bag of n such that
A6: f reduces_to g,p,b,T by A5;
consider s being bag of n such that
s + (HT (p,T)) = b and
A7: g = f - (((f . b) / (HC (p,T))) * (s *' p)) by A6;
reconsider P = P as non empty Subset of (Polynom-Ring (n,L)) by A4;
set q = ((f . b) / (HC (p,T))) * (s *' p);
set q9 = (Monom (((f . b) / (HC (p,T))),s)) *' p;
set r = <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*>;

now :: thesis: for u being object st u in rng <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*> holds
u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in rng <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*> implies u in the carrier of (Polynom-Ring (n,L)) )
A8: rng <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*> = {((Monom (((f . b) / (HC (p,T))),s)) *' p)} by FINSEQ_1:39;
assume u in rng <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*> ; :: thesis: u in the carrier of (Polynom-Ring (n,L))
then u = (Monom (((f . b) / (HC (p,T))),s)) *' p by A8, TARSKI:def 1;
hence u in the carrier of (Polynom-Ring (n,L)) by POLYNOM1:def 11; :: thesis: verum

end;

then rng <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*> c= the carrier of (Polynom-Ring (n,L)) by TARSKI:def 3;
then reconsider r = <*((Monom (((f . b) / (HC (p,T))),s)) *' p)*> as FinSequence of the carrier of (Polynom-Ring (n,L)) by FINSEQ_1:def 4;

now :: thesis: for i being set st i in dom r holds
ex u, v being Element of (Polynom-Ring (n,L)) ex a being Element of P st r /. i = (u * a) * v

reconsider p9 = p as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider m = Monom (((f . b) / (HC (p,T))),s) as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
let i be set ; :: thesis: ( i in dom r implies ex u, v being Element of (Polynom-Ring (n,L)) ex a being Element of P st r /. i = (u * a) * v )
assume A9: i in dom r ; :: thesis: ex u, v being Element of (Polynom-Ring (n,L)) ex a being Element of P st r /. i = (u * a) * v
reconsider p9 = p9 as Element of (Polynom-Ring (n,L)) ;
reconsider m = m as Element of (Polynom-Ring (n,L)) ;
A10: (m * p9) * (1. (Polynom-Ring (n,L))) = m * p9
.= (Monom (((f . b) / (HC (p,T))),s)) *' p by POLYNOM1:def 11 ;
dom r = Seg 1 by FINSEQ_1:38;
then i = 1 by A9, FINSEQ_1:2, TARSKI:def 1;
then r . i = (Monom (((f . b) / (HC (p,T))),s)) *' p ;
hence ex u, v being Element of (Polynom-Ring (n,L)) ex a being Element of P st r /. i = (u * a) * v by A4, A9, A10, PARTFUN1:def 6; :: thesis: verum

end;

then reconsider r = r as LinearCombination of P by IDEAL_1:def 8;
(Monom (((f . b) / (HC (p,T))),s)) *' p is Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
then A11: Sum r = (Monom (((f . b) / (HC (p,T))),s)) *' p by BINOM:3;
(Monom (((f . b) / (HC (p,T))),s)) *' p = ((f . b) / (HC (p,T))) * (s *' p) by Th22;
then A12: ((f . b) / (HC (p,T))) * (s *' p) in P -Ideal by A11, IDEAL_1:60;
A13: f - g = f + (- g) by POLYNOM1:def 7
.= f9 + (- g9) by A1, A3, POLYNOM1:def 11
.= f9 - g9 ;
A14: - (- (((f . b) / (HC (p,T))) * (s *' p))) = ((f . b) / (HC (p,T))) * (s *' p) by POLYNOM1:19;
f - g = f + (- (f - (((f . b) / (HC (p,T))) * (s *' p)))) by A7, POLYNOM1:def 7
.= f + (- (f + (- (((f . b) / (HC (p,T))) * (s *' p))))) by POLYNOM1:def 7
.= f + ((- f) + (- (- (((f . b) / (HC (p,T))) * (s *' p))))) by Th1
.= (f + (- f)) + (((f . b) / (HC (p,T))) * (s *' p)) by A14, POLYNOM1:21
.= (0_ (n,L)) + (((f . b) / (HC (p,T))) * (s *' p)) by Th3
.= ((f . b) / (HC (p,T))) * (s *' p) by Th2 ;
hence f9,g9 are_congruent_mod P -Ideal by A12, A13; :: thesis: verum