∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] [inst_3 : Algebra R S],
  algebraMap (AddMonoidAlgebra R M) (AddMonoidAlgebra S M) = AddMonoidAlgebra.mapRangeRingHom M (algebraMap R S)