∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_3} {E₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (motive : (x x_1 : E ≃ₛₗᵢ[σ₁₂] E₂) → x.toLinearEquiv = x_1.toLinearEquiv → Prop) (x x_1 : E ≃ₛₗᵢ[σ₁₂] E₂)
  (x_2 : x.toLinearEquiv = x_1.toLinearEquiv),
  (∀ (toLinearEquiv : E ≃ₛₗ[σ₁₂] E₂) (norm_map' norm_map'_1 : ∀ (x : E), ‖toLinearEquiv x‖ = ‖x‖),
      motive { toLinearEquiv := toLinearEquiv, norm_map' := norm_map' }
        { toLinearEquiv := toLinearEquiv, norm_map' := norm_map'_1 } ⋯) →
    motive x x_1 x_2