let A be non degenerated commutative Ring; :: thesis: for I, q being Ideal of A st q c= I holds
(canHom q) " ((canHom q) .: I) = I
let I, q be Ideal of A; :: thesis: ( q c= I implies (canHom q) " ((canHom q) .: I) = I )
assume q c= I ; :: thesis: (canHom q) " ((canHom q) .: I) = I
then ( ker (canHom q) = q & q c= I ) by RING_2:13;
then A2: I + (ker (canHom q)) c= I by IDEAL_1:75;
(canHom q) " ((canHom q) .: I) c= I

proof

for x being object st x in (canHom q) " ((canHom q) .: I) holds
x in I

proof

set f = canHom q;
let x be object ; :: thesis: ( x in (canHom q) " ((canHom q) .: I) implies x in I )
assume A4: x in (canHom q) " ((canHom q) .: I) ; :: thesis: x in I
then A5: ( x in dom (canHom q) & (canHom q) . x in (canHom q) .: I ) by FUNCT_1:def 7;
consider x1 being object such that
A6: x1 in dom (canHom q) and
A7: x1 in I and
A8: (canHom q) . x = (canHom q) . x1 by A5, FUNCT_1:def 6;
reconsider a = x, b = x1 as Element of A by A4, A6;
((canHom q) . a) - ((canHom q) . b) = 0. (A / q) by A8, RLVECT_1:5;
then (canHom q) . (a - b) = 0. (A / q) by RING_2:8;
then a - b in { v where v is Element of A : (canHom q) . v = 0. (A / q) } ;
then a - b in ker (canHom q) by VECTSP10:def 9;
then consider x3 being object such that
A10: x3 in ker (canHom q) and
A11: x3 = a - b ;
reconsider c = x3 as Element of A by A10;
A12: a = b + c by A11, VECTSP_2:2;
I + (ker (canHom q)) = { (a + b) where a, b is Element of A : ( a in I & b in ker (canHom q) ) } by IDEAL_1:def 19;
then x in I + (ker (canHom q)) by A12, A7, A10;
hence x in I by A2; :: thesis: verum

end;

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

end;

hence (canHom q) " ((canHom q) .: I) = I by FUNCT_2:42; :: thesis: verum