let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic
let f be Homomorphism of R,S; :: thesis: ( f is onto implies R / (ker f),S are_isomorphic )
set B = R / (ker f);
set I = ker f;
set T = Image f;
assume AS: f is onto ; :: thesis: R / (ker f),S are_isomorphic
then A: rng f = the carrier of S by FUNCT_2:def 3;
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) by A ; :: 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) by A ; :: 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;
rng g = the carrier of S by B, AS, FUNCT_2:def 3;
then g is onto by FUNCT_2:def 3;
hence R / (ker f),S are_isomorphic by C; :: thesis: verum