let R be Ring; :: thesis:
let I be Ideal of R; :: thesis:

let xx be object ; :: thesis:
assume AS: xx in ker (canHom I) ; :: thesis:
then reconsider x = xx as Element of R ;
Class ((EqRel (R,I)),(0. R)) = 0. (R / I) by RING_1:def 6
.= (canHom I) . x by AS, ker1
.= Class ((EqRel (R,I)),x) by defhomI ;
then x - (0. R) in I by RING_1:6;
hence xx in I ; :: thesis:

end;

let xx be object ; :: thesis:
assume AS: xx in I ; :: thesis:
then reconsider x = xx as Element of R ;
x - (0. R) in I by AS;
then B: Class ((EqRel (R,I)),x) = Class ((EqRel (R,I)),(0. R)) by RING_1:6;
(canHom I) . x = Class ((EqRel (R,I)),x) by defhomI
.= 0. (R / I) by B, RING_1:def 6 ;
hence xx in ker (canHom I) ; :: thesis:

end;