∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (carrier : Set P)
  (smul_vsub_vadd_mem :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier → p₂ ∈ carrier → p₃ ∈ carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier)
  (carrier_1 : Set P)
  (smul_vsub_vadd_mem_1 :
    ∀ (c : k) {p₁ p₂ p₃ : P}, p₁ ∈ carrier_1 → p₂ ∈ carrier_1 → p₃ ∈ carrier_1 → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ carrier_1),
  ({ carrier := carrier, smul_vsub_vadd_mem := smul_vsub_vadd_mem } =
      { carrier := carrier_1, smul_vsub_vadd_mem := smul_vsub_vadd_mem_1 }) =
    (carrier = carrier_1)