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