fact: Definition set_surj_fun_on (aT rT: finType) (B: {set rT}):= [set f: {ffun aT -> rT} | f @: aT == B ].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)