{𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] →
              [inst_4 : NormedAddTorsor V P] →
                (s₁ s₂ : AffineSubspace 𝕜 P) →
                  [inst_5 : Nonempty ↥s₁] → [inst_6 : Nonempty ↥s₂] → s₁ = s₂ → ↥s₁ ≃ᵃⁱ[𝕜] ↥s₂