set g = canHom I;
set B = R / I;

now :: thesis: for a, b being Element of R holds (canHom I) . (a + b) = ((canHom I) . a) + ((canHom I) . b)

let a, b be Element of R; :: thesis: (canHom I) . (a + b) = ((canHom I) . a) + ((canHom I) . b)
reconsider x = Class ((EqRel (R,I)),a) as Element of (R / I) by RING_1:12;
reconsider y = Class ((EqRel (R,I)),b) as Element of (R / I) by RING_1:12;
H1: (canHom I) . a = Class ((EqRel (R,I)),a) by defhomI;
H: x + y = Class ((EqRel (R,I)),(a + b)) by RING_1:13;
thus (canHom I) . (a + b) = x + y by H, defhomI
.= ((canHom I) . a) + ((canHom I) . b) by H1, defhomI ; :: thesis: verum

end;

hence canHom I is additive ; :: thesis: ( canHom I is multiplicative & canHom I is unity-preserving )

now :: thesis: for a, b being Element of R holds (canHom I) . (a * b) = ((canHom I) . a) * ((canHom I) . b)

let a, b be Element of R; :: thesis: (canHom I) . (a * b) = ((canHom I) . a) * ((canHom I) . b)
reconsider x = Class ((EqRel (R,I)),a) as Element of (R / I) by RING_1:12;
reconsider y = Class ((EqRel (R,I)),b) as Element of (R / I) by RING_1:12;
H1: (canHom I) . a = Class ((EqRel (R,I)),a) by defhomI;
H: x * y = Class ((EqRel (R,I)),(a * b)) by RING_1:14;
thus (canHom I) . (a * b) = x * y by H, defhomI
.= ((canHom I) . a) * ((canHom I) . b) by H1, defhomI ; :: thesis: verum

end;

hence canHom I is multiplicative ; :: thesis: canHom I is unity-preserving
(canHom I) . (1. R) = Class ((EqRel (R,I)),(1. R)) by defhomI
.= 1. (R / I) by RING_1:15 ;
hence canHom I is unity-preserving ; :: thesis: verum