∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} {A₁' : Type uA₁'} {A₂' : Type uA₂'} {A₃' : Type uA₃'}
  [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Semiring A₁']
  [inst_5 : Semiring A₂'] [inst_6 : Semiring A₃'] [inst_7 : Algebra R A₁] [inst_8 : Algebra R A₂]
  [inst_9 : Algebra R A₃] [inst_10 : Algebra R A₁'] [inst_11 : Algebra R A₂'] [inst_12 : Algebra R A₃']
  (e₁ : A₁ ≃ₐ[R] A₂) (e₁' : A₁' ≃ₐ[R] A₂') (e₂ : A₂ ≃ₐ[R] A₃) (e₂' : A₂' ≃ₐ[R] A₃'),
  (e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')