let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1 being Ideal of (A / q)
for x, y being Element of the carrier of A st x in (canHom q) " M1 & y in (canHom q) " M1 holds
x + y in (canHom q) " M1
let q be Ideal of A; :: thesis: for M1 being Ideal of (A / q)
for x, y being Element of the carrier of A st x in (canHom q) " M1 & y in (canHom q) " M1 holds
x + y in (canHom q) " M1
let M1 be Ideal of (A / q); :: thesis: for x, y being Element of the carrier of A st x in (canHom q) " M1 & y in (canHom q) " M1 holds
x + y in (canHom q) " M1
let x, y be Element of the carrier of A; :: thesis: ( x in (canHom q) " M1 & y in (canHom q) " M1 implies x + y in (canHom q) " M1 )
assume that
A1: x in (canHom q) " M1 and
A2: y in (canHom q) " M1 ; :: thesis: x + y in (canHom q) " M1
A3: (canHom q) . x in M1 by A1, FUNCT_1:def 7;
A4: (canHom q) . y in M1 by A2, FUNCT_1:def 7;
reconsider a = x, b = y as Element of A ;
reconsider x1 = Class ((EqRel (A,q)),a) as Element of (A / q) by RING_1:12;
reconsider y1 = Class ((EqRel (A,q)),b) as Element of (A / q) by RING_1:12;
((canHom q) . x) + ((canHom q) . y) = x1 + ((canHom q) . y) by RING_2:def 5
.= x1 + y1 by RING_2:def 5
.= Class ((EqRel (A,q)),(a + b)) by RING_1:13 ;
then A5: Class ((EqRel (A,q)),(a + b)) in M1 by A3, A4, IDEAL_1:def 1;
A6: (canHom q) . (a + b) in M1 by A5, RING_2:def 5;
a + b in A ;
then a + b in dom (canHom q) by FUNCT_2:def 1;
hence x + y in (canHom q) " M1 by A6, FUNCT_1:def 7; :: thesis: verum