for A being non degenerated commutative Ring
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