let A be non degenerated commutative Ring; :: thesis: for q being Ideal of A
for M1 being Ideal of (A / q) holds q c= (canHom q) " M1
let q be Ideal of A; :: thesis: for M1 being Ideal of (A / q) holds q c= (canHom q) " M1
let M1 be Ideal of (A / q); :: thesis: q c= (canHom q) " M1
reconsider m = (canHom q) " M1 as Ideal of A by Th22;
for x being object st x in q holds
x in (canHom q) " M1

proof

let x be object ; :: thesis: ( x in q implies x in (canHom q) " M1 )
assume A1: x in q ; :: thesis: x in (canHom q) " M1
then x in the carrier of A ;
then A3: x in dom (canHom q) by FUNCT_2:def 1;
x in ker (canHom q) by A1, RING_2:13;
then x in { v where v is Element of A : (canHom q) . v = 0. (A / q) } by VECTSP10:def 9;
then consider x1 being Element of A such that
A4: x = x1 and
A5: (canHom q) . x1 = 0. (A / q) ;
(canHom q) . x in M1 by A5, A4, IDEAL_1:2;
hence x in (canHom q) " M1 by A3, FUNCT_1:def 7; :: thesis: verum

end;

hence q c= (canHom q) " M1 ; :: thesis: verum