∀ {F : Type u_2} [inst : Field F] {K₁ : Type u_4} {K₂ : Type u_1} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_3) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂] [inst_9 : IsScalarTower F E K₁]
  [inst_10 : IsScalarTower F E K₂] [h : Normal F E] (x y : ↥(IsScalarTower.toAlgHom F E K₁).range),
  ↑⟨ϕ ↑(x * y), ⋯⟩ = ↑(⟨ϕ ↑x, ⋯⟩ * ⟨ϕ ↑y, ⋯⟩)