∀ {P₁ : Type u_6} {P₂ : Type u_1} {P₃ : Type u_7} {P₄ : Type u_2} {V₁ : Type u_8} {V₂ : Type u_3} {V₃ : Type u_9}
  {V₄ : Type u_4} [inst : AddCommGroup V₁] [inst_1 : AddCommGroup V₂] [inst_2 : AddCommGroup V₃]
  [inst_3 : AddCommGroup V₄] [inst_4 : AddTorsor V₁ P₁] [inst_5 : AddTorsor V₂ P₂] [inst_6 : AddTorsor V₃ P₃]
  [inst_7 : AddTorsor V₄ P₄] {R : Type u_5} [inst_8 : CommRing R] [inst_9 : Module R V₁] [inst_10 : Module R V₂]
  [inst_11 : Module R V₃] [inst_12 : Module R V₄] (e₁ : P₁ ≃ᵃ[R] P₂) (e₂ : P₃ ≃ᵃ[R] P₄) (x : P₁ →ᵃ[R] P₃)
  (x_1 : P₁ →ᵃ[R] V₃), (e₁.arrowCongrEquiv e₂) (x_1 +ᵥ x) = (e₁.arrowCongrₗ e₂.linear) x_1 +ᵥ (e₁.arrowCongrEquiv e₂) x