Let X, Tx, n, F and e be given.
Assume HTx: topology_on X Tx.
Assume HnO: n ∈ ω.
Assume Hbij: bijection n F e.
Assume HtermCont: ∀f : set, f ∈ F → continuous_map X Tx R R_standard_topology f.
We prove the intermediate claim HRtop: topology_on R R_standard_topology.
An exact proof term for the current goal is R_standard_topology_is_topology_local.
We prove the intermediate claim Hfun_e: function_on e n F.
An exact proof term for the current goal is (andEL (function_on e n F) (∀y : set, y ∈ F → ∃x : set, x ∈ n ∧ apply_fun e x = y ∧ (∀x' : set, x' ∈ n → apply_fun e x' = y → x' = x)) Hbij).
Set sum_at to be the term (λm : set ⇒ graph X (λx : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) m)).
Set Psum to be the term (λm : set ⇒ m ∈ ordsucc n → continuous_map X Tx R R_standard_topology (sum_at m)).
We prove the intermediate claim HP0: Psum 0.
Assume H0: 0 ∈ ordsucc n.
We will prove continuous_map X Tx R R_standard_topology (sum_at 0).
Set c0 to be the term const_fun X 0.
We prove the intermediate claim Hc0cont: continuous_map X Tx R R_standard_topology c0.
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx HRtop real_0).
Apply (continuous_map_congr_on X Tx R R_standard_topology c0 (sum_at 0)) to the current goal.
An exact proof term for the current goal is Hc0cont.
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) 0) x HxX) (from left to right).
rewrite the current goal using (nat_primrec_0 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x))) (from left to right).
An exact proof term for the current goal is real_0.
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using (const_fun_apply X 0 x HxX) (from left to right).
We prove the intermediate claim Hsum0: sum_at 0 = graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) 0).
Use reflexivity.
rewrite the current goal using Hsum0 (from left to right) at position 1.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) 0) x HxX) (from left to right).
rewrite the current goal using (nat_primrec_0 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x))) (from left to right).
Use reflexivity.
We prove the intermediate claim HPS: ∀m : set, nat_p m → Psum m → Psum (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume IH: Psum m.
Assume HmS: ordsucc m ∈ ordsucc n.
We prove the intermediate claim Hsub: ordsucc m ⊆ n.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
An exact proof term for the current goal is (nat_ordsucc_trans n HnNat (ordsucc m) HmS).
We prove the intermediate claim HmInN: m ∈ n.
An exact proof term for the current goal is (Hsub m (ordsuccI2 m)).
We prove the intermediate claim Hsm: continuous_map X Tx R R_standard_topology (sum_at m).
An exact proof term for the current goal is (IH (ordsuccI1 n m (Hsub m (ordsuccI2 m)))).
Set fm to be the term apply_fun e m.
We prove the intermediate claim HfmF: fm ∈ F.
An exact proof term for the current goal is (Hfun_e m HmInN).
We prove the intermediate claim HfmCont: continuous_map X Tx R R_standard_topology fm.
An exact proof term for the current goal is (HtermCont fm HfmF).
We will prove continuous_map X Tx R R_standard_topology (sum_at (ordsucc m)).
Apply (continuous_map_congr_on X Tx R R_standard_topology (compose_fun X (pair_map X (sum_at m) fm) add_fun_R) (sum_at (ordsucc m))) to the current goal.
An exact proof term for the current goal is (add_two_continuous_R X Tx (sum_at m) fm HTx Hsm HfmCont).
Let x be given.
Assume HxX: x ∈ X.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) (ordsucc m)) x HxX) (from left to right).
rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) m HmNat) (from left to right).
We prove the intermediate claim HprevR: nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) m ∈ R.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) m) x HxX) (from right to left).
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (sum_at m) Hsm x HxX).
We prove the intermediate claim HtermRm: apply_fun (apply_fun e m) x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology fm HfmCont x HxX).
An exact proof term for the current goal is (real_add_SNo (nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) m) HprevR (apply_fun (apply_fun e m) x) HtermRm).
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hlhs: apply_fun (sum_at (ordsucc m)) x = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) (ordsucc m).
We prove the intermediate claim HdefSm: sum_at (ordsucc m) = graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) (ordsucc m)).
Use reflexivity.
rewrite the current goal using HdefSm (from left to right) at position 1.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) (ordsucc m)) x HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hprev: apply_fun (sum_at m) x = nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) m.
We prove the intermediate claim Hdefm: sum_at m = graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) m).
Use reflexivity.
rewrite the current goal using Hdefm (from left to right) at position 1.
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) m) x HxX) (from left to right).
Use reflexivity.
We prove the intermediate claim HsmR: apply_fun (sum_at m) x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (sum_at m) Hsm x HxX).
We prove the intermediate claim HfmR: apply_fun fm x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology fm HfmCont x HxX).
rewrite the current goal using (add_of_pair_map_apply X (sum_at m) fm x HxX HsmR HfmR) (from left to right).
rewrite the current goal using Hlhs (from left to right).
rewrite the current goal using (apply_fun_graph X (λx0 : set ⇒ nat_primrec 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x0)) m) x HxX) (from left to right) at position 1.
rewrite the current goal using (nat_primrec_S 0 (λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)) m HmNat) (from left to right).
Use reflexivity.
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnO).
We prove the intermediate claim HPn: Psum n.
An exact proof term for the current goal is (nat_ind Psum HP0 HPS n HnNat).
We prove the intermediate claim HnIn: n ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI2 n).
An exact proof term for the current goal is (HPn HnIn).
∎