let A be non degenerated commutative Ring; 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; 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); ( 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
; 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; verum