let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1 being Ideal of (A / q) holds (canHom q) " M1 is Ideal of A
let q be Ideal of A; :: thesis: for M1 being Ideal of (A / q) holds (canHom q) " M1 is Ideal of A
let M1 be Ideal of (A / q); :: thesis: (canHom q) " M1 is Ideal of A
A1: (canHom q) " M1 is add-closed by Th20;
A2: (canHom q) " M1 is left-ideal by Th21;
A3: (canHom q) . (0. A) = Class ((EqRel (A,q)),(0. A)) by RING_2:def 5
.= 0. (A / q) by RING_1:def 6 ;
A4: dom (canHom q) = the carrier of A by FUNCT_2:def 1;
(canHom q) . (0. A) in M1 by A3, IDEAL_1:2;
then 0. A in (canHom q) " M1 by A4, FUNCT_1:def 7;
hence (canHom q) " M1 is Ideal of A by A1, A2; :: thesis: verum