- [ apply continuous_relation_comp;
- | intros; simplify; (*intro x; simplify;*)
- change with (b⎻* ∘ (a⎻* ∘ A o1) = b'⎻* ∘ (a'⎻* ∘ A o1));
- change in H with (a⎻* ∘ A o1 = a'⎻* ∘ A o1);
- change in H1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2);
- apply (.= H‡#);
- intro x;
-
- change with (eq1 (oa_P (carrbt o3)) (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x))));
- lapply (saturated o1 o2 a' (A o1 x):?) as X;
- [ apply ((saturation_idempotent ?? (A_is_saturation o1) x)^-1) ]
- change in X with (eq1 (oa_P (carrbt o2)) (a'⎻* (A o1 x)) (A o2 (a'⎻* (A o1 x))));
- unfold uncurry_arrows;
- apply (.= †X); whd in H1;
- lapply (H1 (a'⎻* (A o1 x))) as X1;
- change in X1 with (eq1 (oa_P (carrbt o3)) (b⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻* (A o2 (a' \sup ⎻* (A o1 x)))));
- apply (.= X1);
- unfold uncurry_arrows;
- apply (†(X\sup -1));]
+ [ apply Ocontinuous_relation_comp;
+ | intros; simplify;
+ change with ((b⎻* ∘ a⎻* ) ∘ oA o1 = ((b'⎻* ∘ a'⎻* ) ∘ oA o1));
+ change with (b⎻* ∘ (a⎻* ∘ oA o1) = b'⎻* ∘ (a'⎻* ∘ oA o1));
+ change in e with (a⎻* ∘ oA o1 = a'⎻* ∘ oA o1);
+ change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
+ apply (.= e‡#);
+ intro x;
+ change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x))));
+ apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
+ apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
+ apply (.= (e1 (a'⎻* (oA o1 x))));
+ change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));
+ apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
+ apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
+ apply rule #;]
+ | intros; simplify;
+ change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ oA o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ oA o1));
+ apply rule (#‡ASSOC ^ -1);