let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being Homomorphism of R,S holds R / (ker f), Image f are_isomorphic
let S be R -homomorphic Ring; :: thesis: for f being Homomorphism of R,S holds R / (ker f), Image f are_isomorphic
let f be Homomorphism of R,S; :: thesis: R / (ker f), Image f are_isomorphic
canHom f is RingIsomorphism ;
hence R / (ker f), Image f are_isomorphic ; :: thesis: verum