∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (p₁ p₂ : P × P'), (p₁ -ᵥ p₂).2 = p₁.2 -ᵥ p₂.2