let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1, M2 being Ideal of (A / q) st M1 c= M2 holds
(canHom q) " M1 c= (canHom q) " M2
let q be Ideal of A; :: thesis: for M1, M2 being Ideal of (A / q) st M1 c= M2 holds
(canHom q) " M1 c= (canHom q) " M2
let M1, M2 be Ideal of (A / q); :: thesis: ( M1 c= M2 implies (canHom q) " M1 c= (canHom q) " M2 )
assume A1: M1 c= M2 ; :: thesis: (canHom q) " M1 c= (canHom q) " M2
for x being Element of the carrier of A st x in (canHom q) " M1 holds
x in (canHom q) " M2

proof

let x be Element of the carrier of A; :: thesis: ( x in (canHom q) " M1 implies x in (canHom q) " M2 )
assume x in (canHom q) " M1 ; :: thesis: x in (canHom q) " M2
then ( x in dom (canHom q) & (canHom q) . x in M1 ) by FUNCT_1:def 7;
hence x in (canHom q) " M2 by FUNCT_1:def 7, A1; :: thesis: verum

end;

hence (canHom q) " M1 c= (canHom q) " M2 ; :: thesis: verum