for R being Ring
for S being b₁ -homomorphic Ring
for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic