proposition: Lemma composable_domain : forall f g : E, composable f g -> domain (compose f g) = domain g.
proof: Proof. ir. unfold compose in |- *. rewrite create_domain. ap extensionality. ap inverse_image_sub. unfold sub in |- *; ir. ap inverse_image_inc. am. unfold composable in H. xd. ap H2. ap range_inc. am. apply ex_intro with x. xd. Qed.
imports: set_theory