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)) )

assume that

A1: x = Class ((EqRel (R,I)),a) and

A2: y = Class ((EqRel (R,I)),b) ; :: thesis: x * y = Class ((EqRel (R,I)),(a * b))

consider a1, b1 being Element of R such that

A3: x = Class ((EqRel (R,I)),a1) and

A4: y = Class ((EqRel (R,I)),b1) and

A5: the multF of (R / I) . (x,y) = Class ((EqRel (R,I)),(a1 * b1)) by Def6;

b1 - b in I by A2, A4, Th6;

then A6: a1 * (b1 - b) in I by IDEAL_1:def 2;

( (a1 - a) * b = (a1 * b) - (a * b) & a1 * (b1 - b) = (a1 * b1) - (a1 * b) ) by VECTSP_1:11, VECTSP_1:13;

then A7: (a1 * (b1 - b)) + ((a1 - a) * b) = (((a1 * b1) - (a1 * b)) + (a1 * b)) - (a * b) by RLVECT_1:28

.= (a1 * b1) - (a * b) by Th1 ;

a1 - a in I by A1, A3, Th6;

then (a1 - a) * b in I by IDEAL_1:def 3;

then ((a1 - a) * b) + (a1 * (b1 - b)) in I by A6, IDEAL_1:def 1;

hence x * y = Class ((EqRel (R,I)),(a * b)) by A5, A7, 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)) )

assume that

A1: x = Class ((EqRel (R,I)),a) and

A2: y = Class ((EqRel (R,I)),b) ; :: thesis: x * y = Class ((EqRel (R,I)),(a * b))

consider a1, b1 being Element of R such that

A3: x = Class ((EqRel (R,I)),a1) and

A4: y = Class ((EqRel (R,I)),b1) and

A5: the multF of (R / I) . (x,y) = Class ((EqRel (R,I)),(a1 * b1)) by Def6;

b1 - b in I by A2, A4, Th6;

then A6: a1 * (b1 - b) in I by IDEAL_1:def 2;

( (a1 - a) * b = (a1 * b) - (a * b) & a1 * (b1 - b) = (a1 * b1) - (a1 * b) ) by VECTSP_1:11, VECTSP_1:13;

then A7: (a1 * (b1 - b)) + ((a1 - a) * b) = (((a1 * b1) - (a1 * b)) + (a1 * b)) - (a * b) by RLVECT_1:28

.= (a1 * b1) - (a * b) by Th1 ;

a1 - a in I by A1, A3, Th6;

then (a1 - a) * b in I by IDEAL_1:def 3;

then ((a1 - a) * b) + (a1 * (b1 - b)) in I by A6, IDEAL_1:def 1;

hence x * y = Class ((EqRel (R,I)),(a * b)) by A5, A7, Th6; :: thesis: verum