∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (v v' : V₁) (p : P₁) (c : k),
  (AffineMap.lineMap (v +ᵥ p) (v' +ᵥ p)) c = (AffineMap.lineMap v v') c +ᵥ p