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

proof

let x be Element of the carrier of (A / q); :: thesis: ( x in (canHom q) .: I implies x in (canHom q) .: J )
assume x in (canHom q) .: I ; :: thesis: x in (canHom q) .: J
then consider x0 being object such that
A3: x0 in dom (canHom q) and
A4: x0 in I and
A5: x = (canHom q) . x0 by FUNCT_1:def 6;
thus x in (canHom q) .: J by A5, A1, A4, A3, FUNCT_1:def 6; :: thesis: verum

end;

hence (canHom q) .: I c= (canHom q) .: J ; :: thesis: verum