Let X, F and J be given.
Assume Htot: total_function_on F J (function_space X unit_interval).
We will prove function_on (diagonal_map X F J) X (unit_interval_power J).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HdiagDef: diagonal_map X F J = graph X (λx0 : set ⇒ graph J (λj : set ⇒ apply_fun (apply_fun F j) x0)).
Use reflexivity.
rewrite the current goal using HdiagDef (from left to right) at position 1.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ graph J (λj : set ⇒ apply_fun (apply_fun F j) x0)) x HxX) (from left to right).
Apply (graph_to_unit_interval_in_unit_interval_power J (λj : set ⇒ apply_fun (apply_fun F j) x)) to the current goal.
Let j be given.
Assume HjJ: j ∈ J.
We prove the intermediate claim HFj: apply_fun F j ∈ function_space X unit_interval.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y F J (function_space X unit_interval) j Htot HjJ).
We prove the intermediate claim HFjFun: function_on (apply_fun F j) X unit_interval.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod X unit_interval)) (λf0 : set ⇒ function_on f0 X unit_interval) (apply_fun F j) HFj).
An exact proof term for the current goal is (HFjFun x HxX).
∎