(p : ENNReal) →
  {ι : Type u_2} →
    (α : ι → Type u_3) →
      [inst : Fact (1 ≤ p)] →
        [inst_1 : Fintype ι] →
          [inst_2 : (i : ι) → SeminormedAddCommGroup (α i)] →
            {R : Type u_5} → [inst_3 : NormedField R] → [(i : ι) → NormedSpace R (α i)] → NormedSpace R ((i : ι) → α i)