let R be Ring; for I being Ideal of R
for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
let I be Ideal of R; for a, b being Element of R
for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
let a, b be Element of R; for x, y being Element of (R / I) st x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) holds
x + y = Class ((EqRel (R,I)),(a + b))
let x, y be Element of (R / I); ( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) implies x + y = Class ((EqRel (R,I)),(a + b)) )
consider a1, b1 being Element of R such that
A1:
( x = Class ((EqRel (R,I)),a1) & y = Class ((EqRel (R,I)),b1) )
and
A2:
the addF of (R / I) . (x,y) = Class ((EqRel (R,I)),(a1 + b1))
by Def6;
A3: (a1 - a) + (b1 - b) =
((a1 - a) + b1) - b
by RLVECT_1:28
.=
((a1 + b1) - a) - b
by RLVECT_1:28
.=
(a1 + b1) - (a + b)
by RLVECT_1:27
;
assume
( x = Class ((EqRel (R,I)),a) & y = Class ((EqRel (R,I)),b) )
; x + y = Class ((EqRel (R,I)),(a + b))
then
( a1 - a in I & b1 - b in I )
by A1, Th6;
then
(a1 + b1) - (a + b) in I
by A3, IDEAL_1:def 1;
hence
x + y = Class ((EqRel (R,I)),(a + b))
by A2, Th6; verum