Let J, f, g and a be given.
Assume Hf: f ∈ power_real J.
Assume Hg: g ∈ power_real J.
Assume HaA: a ∈ power_real_clipped_diffs J f g.
We will prove a ∈ R.
Apply (ReplE_impred J (λj : set ⇒ power_real_coord_clipped_diff f g j) a HaA (a ∈ R)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
Assume Haj: a = power_real_coord_clipped_diff f g j.
rewrite the current goal using Haj (from left to right).
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).
We prove the intermediate claim HfjR: apply_fun f j ∈ R.
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.
We prove the intermediate claim Hgpred: total_function_on g J (space_family_union J (const_space_family J R R_standard_topology)) ∧ functional_graph g ∧ ∀i0 : set, i0 ∈ J → apply_fun g 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)))) (λg0 : set ⇒ total_function_on g0 J (space_family_union J (const_space_family J R R_standard_topology)) ∧ functional_graph g0 ∧ ∀i0 : set, i0 ∈ J → apply_fun g0 i0 ∈ space_family_set (const_space_family J R R_standard_topology) i0) g Hg).
We prove the intermediate claim Hgcoords: ∀i0 : set, i0 ∈ J → apply_fun g 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 g J (space_family_union J (const_space_family J R R_standard_topology)) ∧ functional_graph g) (∀i0 : set, i0 ∈ J → apply_fun g i0 ∈ space_family_set (const_space_family J R R_standard_topology) i0) Hgpred).
We prove the intermediate claim HgjSet: apply_fun g j ∈ space_family_set (const_space_family J R R_standard_topology) j.
An exact proof term for the current goal is (Hgcoords j HjJ).
We prove the intermediate claim HgjR: apply_fun g j ∈ R.
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 HgjSet.
rewrite the current goal using (power_real_coord_clipped_diff_eq_R_bounded_distance J f g j HjJ Hf Hg) (from left to right).
An exact proof term for the current goal is (R_bounded_distance_in_R (apply_fun f j) (apply_fun g j) HfjR HgjR).
∎