proposition: Lemma morphimIim A : f @* D :&: f @* A = f @* A.
proof: Proof. by apply/setIidPr; rewrite imsetS // setIid subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)