let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A holds (canHom q) " ([#] (A / q)) = [#] A
let q be Ideal of A; :: thesis: (canHom q) " ([#] (A / q)) = [#] A
(canHom q) " ([#] (A / q)) = (canHom q) " (rng (canHom q)) by FUNCT_2:def 3
.= dom (canHom q) by RELAT_1:134
.= [#] A by FUNCT_2:def 1 ;
hence (canHom q) " ([#] (A / q)) = [#] A ; :: thesis: verum