+
+lemma extS_com: ∀o1,o2,o3,c1,c2,S. extS o1 o3 (c1 ∘ c2) S = extS o1 o2 c1 (extS o2 o3 c2 S).
+ intros; unfold extS; simplify; split; intros; simplify; intros;
+ [ cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+ cases H3 (H4 H5); cases H5 (w1 H6); clear H3 H5; cases H6 (H7 H8); clear H6;
+ exists; [apply w1] split [2: assumption] constructor 1; [assumption]
+ exists; [apply w] split; assumption
+ | cases f (H1 H2); cases H2 (w H3); clear f H2; split; [assumption]
+ cases H3 (H4 H5); cases H4 (w1 H6); clear H3 H4; cases H6 (w2 H7); clear H6;
+ cases H7; clear H7; exists; [apply w2] split; [assumption] exists [apply w] split;
+ assumption]
+qed.
+
+definition convergent_relation_space_composition:
+ ∀o1,o2,o3: concrete_space.
+ binary_morphism1
+ (convergent_relation_space_setoid o1 o2)
+ (convergent_relation_space_setoid o2 o3)
+ (convergent_relation_space_setoid o1 o3).
+ intros; constructor 1;
+ [ intros; whd in c c1 ⊢ %;
+ constructor 1;
+ [ apply (fun1 ??? (comp1 BP ???)); [apply (bp o2) |*: apply rp; assumption]
+ | intros;
+ change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+ change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? (? ? ? (? ? ? %) ?) ?)))
+ with (c \sub \f ∘ c1 \sub \f);
+ change in ⊢ (? ? ? ? (? ? ? ? (? ? ? ? ? ? (? ? ? (? ? ? %) ?))))
+ with (c \sub \f ∘ c1 \sub \f);
+ apply (.= (extS_com ??????));
+ apply (.= (†(respects_converges ?????)));
+ apply (.= (respects_converges ?????));
+ apply (.= (†(((extS_com ??????) \sup -1)‡(extS_com ??????)\sup -1)));
+ apply refl1;
+ | change in ⊢ (? ? ? (? ? ? (? ? ? %) ?) ?) with (c \sub \c ∘ c1 \sub \c);
+ apply (.= (extS_com ??????));
+ apply (.= (†(respects_all_covered ???)));
+ apply (.= respects_all_covered ???);
+ apply refl1]
+ | intros;
+ change with (a ∘ b = a' ∘ b');
+ change in H with (rp'' ?? a = rp'' ?? a');
+ change in H1 with (rp'' ?? b = rp ?? b');
+ apply (.= (H‡H1));
+ apply refl1]
+qed.
+