proposition: Lemma range_compose (f : A -> B) (g : B -> C) : range f U V -> range g V W -> range (compose g f) U W.
proof: Proof. intros Hf Hg x Hx. apply Hg, Hf, Hx. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)