(E : Type u_2) →
  (F : Type u_3) →
    {inst : NormedAddCommGroup E} →
      {inst_1 : NormedSpace ℝ E} →
        {inst_2 : NormedAddCommGroup F} →
          {inst_3 : NormedSpace ℝ F} →
            (n : ℕ∞) →
              (K : TopologicalSpace.Compacts E) → [SizeOf E] → [SizeOf F] → SizeOf (ContDiffMapSupportedIn E F n K)