g * f is onto by FUNCT_2:27;
hence for b₁ being Function of R1,R3 st b₁ = g * f holds
b₁ is RingIsomorphism ; :: thesis: verum