proposition: Lemma morphim_set1 x : x \in D -> f @* [set x] = [set f x].
proof: Proof. by rewrite /morphim -sub1set => /setIidPr->; apply: imset_set1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)