let A be non degenerated commutative Ring; :: thesis: for I, q being Ideal of A
for x, y being Element of the carrier of (A / q) st x in (canHom q) .: I & y in (canHom q) .: I holds
x + y in (canHom q) .: I
let I, q be Ideal of A; :: thesis: for x, y being Element of the carrier of (A / q) st x in (canHom q) .: I & y in (canHom q) .: I holds
x + y in (canHom q) .: I
let x, y be Element of the carrier of (A / q); :: thesis: ( x in (canHom q) .: I & y in (canHom q) .: I implies x + y in (canHom q) .: I )
assume that
A1: x in (canHom q) .: I and
A2: y in (canHom q) .: I ; :: thesis: x + y in (canHom q) .: I
consider x0 being object such that
A3: x0 in dom (canHom q) and
A4: x0 in I and
A5: x = (canHom q) . x0 by A1, FUNCT_1:def 6;
consider y0 being object such that
A6: y0 in dom (canHom q) and
A7: y0 in I and
A8: y = (canHom q) . y0 by A2, FUNCT_1:def 6;
A9: dom (canHom q) = the carrier of A by FUNCT_2:def 1;
reconsider x1 = x0, y1 = y0 as Element of A by A3, A6;
A10: (canHom q) . x1 = Class ((EqRel (A,q)),x1) by RING_2:def 5;
A11: (canHom q) . y1 = Class ((EqRel (A,q)),y1) by RING_2:def 5;
A12: x1 + y1 in I by A4, A7, IDEAL_1:def 1;
(canHom q) . (x1 + y1) = Class ((EqRel (A,q)),(x1 + y1)) by RING_2:def 5
.= ((canHom q) . x1) + ((canHom q) . y1) by A10, A11, RING_1:13 ;
hence x + y in (canHom q) .: I by A5, A8, A9, FUNCT_1:def 6, A12; :: thesis: verum