let R be Ring; :: thesis: for I being Ideal of R holds ker (canHom I) = I
let I be Ideal of R; :: thesis: ker (canHom I) = I

A: now :: thesis: for xx being object st xx in ker (canHom I) holds
xx in I

let xx be object ; :: thesis: ( xx in ker (canHom I) implies xx in I )
assume AS: xx in ker (canHom I) ; :: thesis: xx in I
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: verum

end;

now :: thesis: for xx being object st xx in I holds
xx in ker (canHom I)

let xx be object ; :: thesis: ( xx in I implies xx in ker (canHom I) )
assume AS: xx in I ; :: thesis: xx in ker (canHom I)
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: verum

end;

hence ker (canHom I) = I by A, TARSKI:2; :: thesis: verum