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