Let f be given.
Assume Hf: f ∈ real_sequences.
We prove the intermediate claim Hpack: total_function_on f ω R ∧ functional_graph f.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) f Hf).
An exact proof term for the current goal is (andER (total_function_on f ω R) (functional_graph f) Hpack).
∎