fact: Definition range_restr (H : range) : { x : A | In U x } -> { y : B | In V y } := fun p : { x : A | In U x } => exist (fun y : B => In V y) (f (proj1_sig p)) (H (proj1_sig p) (proj2_sig p)).
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)