∀ {R : Type u_2} {S : Type u_1} (f : R → S),
  Function.Surjective f →
    ∀ [inst : Add S] [inst_1 : Mul S] [inst_2 : Distrib R],
      (∀ (x y : R), f (x + y) = f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → RightDistribClass S