{𝓕 : Type u_11} →
  {R : Type u_12} →
    {R₂ : Type u_13} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₂] →
          {σ₁₂ : R →+* R₂} →
            {E : Type u_14} →
              {E₂ : Type u_15} →
                [inst_2 : SeminormedAddCommGroup E] →
                  [inst_3 : SeminormedAddCommGroup E₂] →
                    [inst_4 : Module R E] →
                      [inst_5 : Module R₂ E₂] →
                        [inst_6 : FunLike 𝓕 E E₂] →
                          {motive : SemilinearIsometryClass 𝓕 σ₁₂ E E₂ → Sort u} →
                            ([toSemilinearMapClass : SemilinearMapClass 𝓕 σ₁₂ E E₂] →
                                (norm_map : ∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖) → motive ⋯) →
                              (t : SemilinearIsometryClass 𝓕 σ₁₂ E E₂) → motive t