:: deftheorem Def6 defines QuotientRing RING_1:def 6 :
for R being non empty right_complementable distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
for I being Ideal of R
for b₃ being strict doubleLoopStr holds
( b₃ = QuotientRing (R,I) iff ( the carrier of b₃ = Class (EqRel (R,I)) & 1. b₃ = Class ((EqRel (R,I)),(1. R)) & 0. b₃ = Class ((EqRel (R,I)),(0. R)) & ( for x, y being Element of b₃ ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the addF of b₃ . (x,y) = Class ((EqRel (R,I)),(a + b)) ) ) & ( for x, y being Element of b₃ ex a, b being Element of R st
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) & the multF of b₃ . (x,y) = Class ((EqRel (R,I)),(a * b)) ) ) ) );