apply Integrable.integrableOn
case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)
case this.hfs.h
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x