proposition: Lemma range_char_Im : range <-> Included (Im U f) V.
proof: Proof. rewrite range_char_inverse_image. symmetry. apply inverse_image_Im_adjoint. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)