set g = canHom f;
set A = R / (ker f);
set B = Image f;
set I = ker f;

now :: thesis: for x, y being Element of (R / (ker f)) holds (canHom f) . (x + y) = ((canHom f) . x) + ((canHom f) . y)

let x, y be Element of (R / (ker f)); :: thesis: (canHom f) . (x + y) = ((canHom f) . x) + ((canHom f) . y)
consider a being Element of R such that
H1: x = Class ((EqRel (R,(ker f))),a) by RING_1:11;
consider b being Element of R such that
H2: y = Class ((EqRel (R,(ker f))),b) by RING_1:11;
H3: (canHom f) . x = f . a by H1, ch;
H4: (canHom f) . y = f . b by H2, ch;
x + y = Class ((EqRel (R,(ker f))),(a + b)) by H1, H2, RING_1:13;
hence (canHom f) . (x + y) = f . (a + b) by ch
.= (f . a) + (f . b) by VECTSP_1:def 20
.= ((canHom f) . x) + ((canHom f) . y) by H3, H4, T5 ;
:: thesis: verum

end;

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

now :: thesis: for x, y being Element of (R / (ker f)) holds (canHom f) . (x * y) = ((canHom f) . x) * ((canHom f) . y)

let x, y be Element of (R / (ker f)); :: thesis: (canHom f) . (x * y) = ((canHom f) . x) * ((canHom f) . y)
consider a being Element of R such that
H1: x = Class ((EqRel (R,(ker f))),a) by RING_1:11;
consider b being Element of R such that
H2: y = Class ((EqRel (R,(ker f))),b) by RING_1:11;
H3: (canHom f) . x = f . a by H1, ch;
H4: (canHom f) . y = f . b by H2, ch;
x * y = Class ((EqRel (R,(ker f))),(a * b)) by H1, H2, RING_1:14;
hence (canHom f) . (x * y) = f . (a * b) by ch
.= (f . a) * (f . b) by GROUP_6:def 6
.= ((canHom f) . x) * ((canHom f) . y) by H3, H4, T5 ;
:: thesis: verum

end;

hence canHom f is multiplicative ; :: thesis: canHom f is unity-preserving
(canHom f) . (1. (R / (ker f))) = (canHom f) . (Class ((EqRel (R,(ker f))),(1. R))) by RING_1:15
.= f . (1_ R) by ch
.= 1_ S by GROUP_1:def 13
.= 1. (Image f) by defim ;
hence canHom f is unity-preserving ; :: thesis: verum