∀ {k : Type u_5} {V1 : Type u_3} {P1 : Type u_4} {V2 : Type u_1} {P2 : Type u_2} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2) (p : P1) (v : V1),
  (f +ᵥ g) (v +ᵥ p) -ᵥ g (v +ᵥ p) = ((f +ᵥ g).linear - g.linear) v +ᵥ (f +ᵥ g) p -ᵥ g p