fact: Definition induced_function2: quotient R -> quotient S := induced_function projf equivR projf_well_defined.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec