Let J, f and j be given.

Assume HjJ: j ∈ J.

Assume Hf: f ∈ power_real J.

We will prove apply_fun f j ∈ R.

We prove the intermediate claim Hfpred: total_function_on f J (space_family_union J (const_space_family J R R_standard_topology)) ∧ functional_graph f ∧ ∀i0 : set, i0 ∈ J → apply_fun f i0 ∈ space_family_set (const_space_family J R R_standard_topology) i0.

An exact proof term for the current goal is (SepE2 (𝒫 (setprod J (space_family_union J (const_space_family J R R_standard_topology)))) (λf0 : set ⇒ total_function_on f0 J (space_family_union J (const_space_family J R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i0 : set, i0 ∈ J → apply_fun f0 i0 ∈ space_family_set (const_space_family J R R_standard_topology) i0) f Hf).

We prove the intermediate claim Hfcoords: ∀i0 : set, i0 ∈ J → apply_fun f i0 ∈ space_family_set (const_space_family J R R_standard_topology) i0.

An exact proof term for the current goal is (andER (total_function_on f J (space_family_union J (const_space_family J R R_standard_topology)) ∧ functional_graph f) (∀i0 : set, i0 ∈ J → apply_fun f i0 ∈ space_family_set (const_space_family J R R_standard_topology) i0) Hfpred).

We prove the intermediate claim HfjSet: apply_fun f j ∈ space_family_set (const_space_family J R R_standard_topology) j.

An exact proof term for the current goal is (Hfcoords j HjJ).

rewrite the current goal using (space_family_set_const_space_family J R R_standard_topology j HjJ) (from right to left).

An exact proof term for the current goal is HfjSet.

∎