proposition: Lemma morphimJ A x : x \in D -> f @* (A :^ x) = f @* A :^ f x.
proof: Proof. move=> Dx; rewrite !conjsgE morphimMl ?(morphimMr, sub1set, groupV) //. by rewrite !(morphim_set1, groupV, morphV). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)