∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra S T] (x x_1 : Polynomial R),
  (fun z => (algebraMap S T) ((Polynomial.aeval z) (x * x_1))) =
    (fun z => (algebraMap S T) ((Polynomial.aeval z) x)) * fun z => (algebraMap S T) ((Polynomial.aeval z) x_1)