Let X, Tx, F, n and e be given.
Assume HTx: topology_on X Tx.
Assume HnO: n ∈ ω.
Assume Hbij: bijection n F e.
Assume HcontF: ∀f : set, f ∈ F → continuous_map X Tx R R_standard_topology f.
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 HeFun: 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_step to be the term (λx : set ⇒ λk acc : set ⇒ add_SNo acc (apply_fun (apply_fun e k) x)).
Set partial_sum to be the term (λx m : set ⇒ nat_primrec 0 (sum_step x) m).
Set Pw to be the term (λm : set ⇒ m ∈ ordsucc n → continuous_map X Tx R R_standard_topology (graph X (λx : set ⇒ partial_sum x m))).
We prove the intermediate claim Hbase: Pw 0.
Assume H0In: 0 ∈ ordsucc n.
We prove the intermediate claim Hc0: continuous_map X Tx R R_standard_topology (const_fun X 0).
An exact proof term for the current goal is (const_fun_continuous X Tx R R_standard_topology 0 HTx R_standard_topology_is_topology_local real_0).
We prove the intermediate claim Hg0fun: function_on (graph X (λx : set ⇒ partial_sum x 0)) X R.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun (graph X (λx0 : set ⇒ partial_sum x0 0)) x ∈ R.
We prove the intermediate claim Happ: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 0)) x = partial_sum x 0.
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 0) x HxX).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
An exact proof term for the current goal is real_0.
We prove the intermediate claim Heq0: ∀x : set, x ∈ X → apply_fun (const_fun X 0) x = apply_fun (graph X (λx0 : set ⇒ partial_sum x0 0)) x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim Hconst: apply_fun (const_fun X 0) x = 0.
An exact proof term for the current goal is (const_fun_apply X 0 x HxX).
rewrite the current goal using Hconst (from left to right).
We prove the intermediate claim Happ: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 0)) x = partial_sum x 0.
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 0) x HxX).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hdef0: partial_sum x 0 = nat_primrec 0 (sum_step x) 0.
Use reflexivity.
rewrite the current goal using Hdef0 (from left to right).
rewrite the current goal using (nat_primrec_0 0 (sum_step x)) (from left to right).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology (const_fun X 0) (graph X (λx : set ⇒ partial_sum x 0)) Hc0 Hg0fun Heq0).
We prove the intermediate claim Hstep: ∀m : set, nat_p m → Pw m → Pw (ordsucc m).
Let m be given.
Assume HmNat: nat_p m.
Assume IH: Pw m.
Assume HmSIn: ordsucc m ∈ ordsucc n.
We prove the intermediate claim Hsub: ordsucc m ⊆ n.
An exact proof term for the current goal is (nat_ordsucc_trans n HnNat (ordsucc m) HmSIn).
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 HmInSuccN: m ∈ ordsucc n.
An exact proof term for the current goal is (ordsuccI1 n m HmInN).
We prove the intermediate claim HsumCont: continuous_map X Tx R R_standard_topology (graph X (λx : set ⇒ partial_sum x m)).
An exact proof term for the current goal is (IH HmInSuccN).
We prove the intermediate claim HfkF: apply_fun e m ∈ F.
An exact proof term for the current goal is (HeFun m HmInN).
We prove the intermediate claim HfkCont: continuous_map X Tx R R_standard_topology (apply_fun e m).
An exact proof term for the current goal is (HcontF (apply_fun e m) HfkF).
We prove the intermediate claim HtmpCont: continuous_map X Tx R R_standard_topology (compose_fun X (pair_map X (graph X (λx : set ⇒ partial_sum x m)) (apply_fun e m)) add_fun_R).
An exact proof term for the current goal is (add_two_continuous_R X Tx (graph X (λx : set ⇒ partial_sum x m)) (apply_fun e m) HTx HsumCont HfkCont).
We prove the intermediate claim HgSfun: function_on (graph X (λx : set ⇒ partial_sum x (ordsucc m))) X R.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun (graph X (λx0 : set ⇒ partial_sum x0 (ordsucc m))) x ∈ R.
We prove the intermediate claim HappS: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 (ordsucc m))) x = partial_sum x (ordsucc m).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 (ordsucc m)) x HxX).
rewrite the current goal using HappS (from left to right).
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim HaccR: partial_sum x m ∈ R.
We prove the intermediate claim Happm: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 m)) x = partial_sum x m.
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 m) x HxX).
rewrite the current goal using Happm (from right to left).
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (graph X (λx0 : set ⇒ partial_sum x0 m)) HsumCont x HxX).
We prove the intermediate claim HvalR: 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 (apply_fun e m) HfkCont x HxX).
We prove the intermediate claim HstepDef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (apply_fun e m) x).
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
An exact proof term for the current goal is (real_add_SNo (partial_sum x m) HaccR (apply_fun (apply_fun e m) x) HvalR).
We prove the intermediate claim HeqS: ∀x : set, x ∈ X → apply_fun (compose_fun X (pair_map X (graph X (λx0 : set ⇒ partial_sum x0 m)) (apply_fun e m)) add_fun_R) x = apply_fun (graph X (λx0 : set ⇒ partial_sum x0 (ordsucc m))) x.
Let x be given.
Assume HxX: x ∈ X.
We prove the intermediate claim HsumR: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 m)) x ∈ R.
An exact proof term for the current goal is (continuous_map_function_on X Tx R R_standard_topology (graph X (λx0 : set ⇒ partial_sum x0 m)) HsumCont x HxX).
We prove the intermediate claim HfkR: 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 (apply_fun e m) HfkCont x HxX).
We prove the intermediate claim Hadd: apply_fun (compose_fun X (pair_map X (graph X (λx0 : set ⇒ partial_sum x0 m)) (apply_fun e m)) add_fun_R) x = add_SNo (apply_fun (graph X (λx0 : set ⇒ partial_sum x0 m)) x) (apply_fun (apply_fun e m) x).
An exact proof term for the current goal is (add_of_pair_map_apply X (graph X (λx0 : set ⇒ partial_sum x0 m)) (apply_fun e m) x HxX HsumR HfkR).
rewrite the current goal using Hadd (from left to right).
We prove the intermediate claim Happm: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 m)) x = partial_sum x m.
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 m) x HxX).
rewrite the current goal using Happm (from left to right).
We prove the intermediate claim HappS: apply_fun (graph X (λx0 : set ⇒ partial_sum x0 (ordsucc m))) x = partial_sum x (ordsucc m).
An exact proof term for the current goal is (apply_fun_graph X (λx0 : set ⇒ partial_sum x0 (ordsucc m)) x HxX).
rewrite the current goal using HappS (from left to right).
We prove the intermediate claim HdefS: partial_sum x (ordsucc m) = nat_primrec 0 (sum_step x) (ordsucc m).
Use reflexivity.
rewrite the current goal using HdefS (from left to right).
We prove the intermediate claim HprimS: nat_primrec 0 (sum_step x) (ordsucc m) = sum_step x m (nat_primrec 0 (sum_step x) m).
An exact proof term for the current goal is (nat_primrec_S 0 (sum_step x) m HmNat).
rewrite the current goal using HprimS (from left to right).
We prove the intermediate claim HaccEq: nat_primrec 0 (sum_step x) m = partial_sum x m.
Use reflexivity.
rewrite the current goal using HaccEq (from left to right).
We prove the intermediate claim HstepDef: sum_step x m (partial_sum x m) = add_SNo (partial_sum x m) (apply_fun (apply_fun e m) x).
Use reflexivity.
rewrite the current goal using HstepDef (from left to right).
Use reflexivity.
An exact proof term for the current goal is (continuous_map_congr_on X Tx R R_standard_topology (compose_fun X (pair_map X (graph X (λx : set ⇒ partial_sum x m)) (apply_fun e m)) add_fun_R) (graph X (λx : set ⇒ partial_sum x (ordsucc m))) HtmpCont HgSfun HeqS).
We prove the intermediate claim Hwsn: Pw n.
An exact proof term for the current goal is (nat_ind Pw Hbase Hstep 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 (Hwsn HnIn).
∎