let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1 being Ideal of (A / q) holds (canHom q) .: ((canHom q) " M1) = M1
let q be Ideal of A; :: thesis: for M1 being Ideal of (A / q) holds (canHom q) .: ((canHom q) " M1) = M1
let M1 be Ideal of (A / q); :: thesis: (canHom q) .: ((canHom q) " M1) = M1
rng (canHom q) = the carrier of (A / q) by FUNCT_2:def 3;
hence (canHom q) .: ((canHom q) " M1) = M1 by FUNCT_1:77; :: thesis: verum