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