∀ {k : Type u_1} {K : Type u_2} {ι : Type u_3} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (p : ℕ),
  Nat.Prime p →
    (∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x => x ^ p) ↑s) →
      ∀ {a : ι → K} (n : ι) [ExpChar k p],
        IntermediateField.adjoin k (Set.range a) = ⊤ →
          (IsTranscendenceBasis k fun i => a ↑i) →
            ∃ i,
              (IsTranscendenceBasis k fun j => a ↑j) ∧ Algebra.IsSeparable (↥(IntermediateField.adjoin k (a '' {i}ᶜ))) K