let R be Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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); :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: verum