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