∀ {R : Type u} {S : Type v} {T : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : NonUnitalNonAssocRing T] (g : S →ₙ+* T) (f : R →ₙ+* S), NonUnitalSubring.map g f.range = (g.comp f).range