proposition: Lemma morphimEsub A : A \subset D -> f @* A = f @: A.
proof: Proof. by move=> sAD; rewrite /morphim (setIidPr sAD). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)