fact: Definition fun_onto := forall b, In DB b -> exists a, In DA a /\ f a = b.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)