let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' 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 f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal
let f be non-zero Polynomial of n,L; :: thesis: for g being Polynomial of n,L
for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal
let g be Polynomial of n,L; :: thesis: for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' & f reduces_to g,P,T holds
f',g' are_congruent_mod P -Ideal
let f', g' be Element of (Polynom-Ring n,L); :: thesis: ( f = f' & g = g' & f reduces_to g,P,T implies f',g' are_congruent_mod P -Ideal )
assume A1: ( f = f' & g = g' ) ; :: thesis: ( not f reduces_to g,P,T or f',g' are_congruent_mod P -Ideal )
assume f reduces_to g,P,T ; :: thesis: f',g' are_congruent_mod P -Ideal
then consider p being Polynomial of n,L such that
A2: ( p in P & f reduces_to g,p,T ) by Def7;
reconsider P = P as non empty Subset of (Polynom-Ring n,L) by A2;
consider b being bag of such that
A3: f reduces_to g,p,b,T by A2, Def6;
consider s being bag of such that
A4: ( s + (HT p,T) = b & g = f - (((f . b) / (HC p,T)) * (s *' p)) ) by A3, Def5;
A5: f - g = f + (- (f - (((f . b) / (HC p,T)) * (s *' p)))) by A4, POLYNOM1:def 23
.= f + (- (f + (- (((f . b) / (HC p,T)) * (s *' p))))) by POLYNOM1:def 23
.= f + ((- f) + (- (- (((f . b) / (HC p,T)) * (s *' p))))) by Th1
.= (f + (- f)) + (((f . b) / (HC p,T)) * (s *' p)) by POLYNOM1:80
.= (0_ n,L) + (((f . b) / (HC p,T)) * (s *' p)) by Th3
.= ((f . b) / (HC p,T)) * (s *' p) by Th2 ;
set R = Polynom-Ring n,L;
set q = ((f . b) / (HC p,T)) * (s *' p);
set q' = (Monom ((f . b) / (HC p,T)),s) *' p;
set r = <*((Monom ((f . b) / (HC p,T)),s) *' p)*>;

now

let u be set ; :: thesis: ( u in rng <*((Monom ((f . b) / (HC p,T)),s) *' p)*> implies u in the carrier of (Polynom-Ring n,L) )
assume A6: u in rng <*((Monom ((f . b) / (HC p,T)),s) *' p)*> ; :: thesis: u in the carrier of (Polynom-Ring n,L)
rng <*((Monom ((f . b) / (HC p,T)),s) *' p)*> = {((Monom ((f . b) / (HC p,T)),s) *' p)} by FINSEQ_1:56;
then u = (Monom ((f . b) / (HC p,T)),s) *' p by A6, TARSKI:def 1;
hence u in the carrier of (Polynom-Ring n,L) by POLYNOM1:def 27; :: 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

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 A7: 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
dom r = Seg 1 by FINSEQ_1:55;
then i = 1 by A7, FINSEQ_1:4, TARSKI:def 1;
then A8: r . i = (Monom ((f . b) / (HC p,T)),s) *' p by FINSEQ_1:57;
reconsider m = Monom ((f . b) / (HC p,T)),s as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider m = m as Element of (Polynom-Ring n,L) ;
reconsider p' = p as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider p' = p' as Element of (Polynom-Ring n,L) ;
(m * p') * (1. (Polynom-Ring n,L)) = m * p' by VECTSP_1:def 13
.= (Monom ((f . b) / (HC p,T)),s) *' p by POLYNOM1:def 27 ;
hence ex u, v being Element of (Polynom-Ring n,L) ex a being Element of P st r /. i = (u * a) * v by A2, A7, A8, PARTFUN1:def 8; :: thesis: verum

end;

then reconsider r = r as LinearCombination of P by IDEAL_1:def 9;
(Monom ((f . b) / (HC p,T)),s) *' p is Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
then A9: 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 A10: ((f . b) / (HC p,T)) * (s *' p) in P -Ideal by A9, IDEAL_1:60;
reconsider x = - g as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider x = x as Element of (Polynom-Ring n,L) ;
x + g' = (- g) + g by A1, POLYNOM1:def 27
.= 0_ n,L by Th3
.= 0. (Polynom-Ring n,L) by POLYNOM1:def 27 ;
then A11: - g' = - g by RLVECT_1:19;
f - g = f + (- g) by POLYNOM1:def 23
.= f' + (- g') by A1, A11, POLYNOM1:def 27
.= f' - g' by RLVECT_1:def 12 ;
hence f',g' are_congruent_mod P -Ideal by A5, A10, Def14; :: thesis: verum