Let X, Tx, net, J, le, J', le' and x be given.
Assume H: net_converges_on X Tx net J le x.
Assume H': net_converges_on X Tx net J' le' x.
We prove the intermediate claim Hpre: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U) H).
We prove the intermediate claim Hpre': topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net ∧ graph_domain_subset net J' ∧ x ∈ X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net ∧ graph_domain_subset net J' ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J' ∧ ∀i : set, i ∈ J' → (i0,i) ∈ le' → apply_fun net i ∈ U) H').
We prove the intermediate claim HABCDE: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J) (x ∈ X) Hpre).
We prove the intermediate claim HABCD: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net) (graph_domain_subset net J) HABCDE).
We prove the intermediate claim HABC: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X) (functional_graph net) HABCD).
We prove the intermediate claim Htot: total_function_on net J X.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J le) (total_function_on net J X) HABC).
We prove the intermediate claim Hdom: graph_domain_subset net J.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net) (graph_domain_subset net J) HABCDE).
We prove the intermediate claim HABCDE': topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net ∧ graph_domain_subset net J'.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net ∧ graph_domain_subset net J') (x ∈ X) Hpre').
We prove the intermediate claim HABCD': topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net) (graph_domain_subset net J') HABCDE').
We prove the intermediate claim HABC': topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X) (functional_graph net) HABCD').
We prove the intermediate claim Htot': total_function_on net J' X.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J' le') (total_function_on net J' X) HABC').
We prove the intermediate claim Hdom': graph_domain_subset net J'.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J' le' ∧ total_function_on net J' X ∧ functional_graph net) (graph_domain_subset net J') HABCDE').
An exact proof term for the current goal is (total_function_on_domain_unique net J J' X Htot Hdom Htot' Hdom').
∎