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:42
.= ((a1 + b1) - a) - b by RLVECT_1:42
.= (a1 + b1) - (a + b) by RLVECT_1:41 ;
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