let R be Ring; :: thesis: R / {(0. R)},R are_isomorphic
id R is RingHomomorphism ;
then reconsider S = R as R -homomorphic Ring by defhom;
reconsider f = id R as Homomorphism of R,S ;
A: ker f = {(0. R)} by ker0;
set B = R / (ker f);
B: rng (canHom f) = the carrier of (Image f) by FUNCT_2:def 3
.= rng f by defim ;
then reconsider g = canHom f as Function of (R / (ker f)),S by FUNCT_2:6;

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

let x, y be Element of (R / (ker f)); :: thesis: g . (x + y) = (g . x) + (g . y)
thus g . (x + y) = ((canHom f) . x) + ((canHom f) . y) by VECTSP_1:def 20
.= ( the addF of S || (rng f)) . (((canHom f) . x),((canHom f) . y)) by defim
.= (g . x) + (g . y) ; :: thesis: verum

end;

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

let x, y be Element of (R / (ker f)); :: thesis: g . (x * y) = (g . x) * (g . y)
thus g . (x * y) = ((canHom f) . x) * ((canHom f) . y) by GROUP_6:def 6
.= ( the multF of S || (rng f)) . (((canHom f) . x),((canHom f) . y)) by defim
.= (g . x) * (g . y) ; :: thesis: verum

end;

g . (1. (R / (ker f))) = (canHom f) . (1_ (R / (ker f)))
.= 1_ (Image f) by GROUP_1:def 13
.= 1. S by defim ;
then C: ( g is additive & g is multiplicative & g is unity-preserving ) by C1, C2;
g is onto by B, FUNCT_2:def 3;
hence R / {(0. R)},R are_isomorphic by A, C; :: thesis: verum