let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1 being Ideal of (A / q)
for r, x being Element of the carrier of A st x in (canHom q) " M1 holds
r * x in (canHom q) " M1
let q be Ideal of A; :: thesis: for M1 being Ideal of (A / q)
for r, x being Element of the carrier of A st x in (canHom q) " M1 holds
r * x in (canHom q) " M1
let M1 be Ideal of (A / q); :: thesis: for r, x being Element of the carrier of A st x in (canHom q) " M1 holds
r * x in (canHom q) " M1
let r, x be Element of the carrier of A; :: thesis: ( x in (canHom q) " M1 implies r * x in (canHom q) " M1 )
assume A1: x in (canHom q) " M1 ; :: thesis: r * x in (canHom q) " M1
A2: (canHom q) . x in M1 by A1, FUNCT_1:def 7;
reconsider a = x, b = r as Element of A ;
reconsider x1 = Class ((EqRel (A,q)),a) as Element of (A / q) by RING_1:12;
reconsider r1 = Class ((EqRel (A,q)),b) as Element of (A / q) by RING_1:12;
((canHom q) . r) * ((canHom q) . x) = r1 * ((canHom q) . x) by RING_2:def 5
.= r1 * x1 by RING_2:def 5
.= Class ((EqRel (A,q)),(a * b)) by RING_1:14 ;
then Class ((EqRel (A,q)),(a * b)) in M1 by A2, IDEAL_1:def 2;
then A4: (canHom q) . (a * b) in M1 by RING_2:def 5;
a * b in A ;
then a * b in dom (canHom q) by FUNCT_2:def 1;
hence r * x in (canHom q) " M1 by A4, FUNCT_1:def 7; :: thesis: verum