proposition: Lemma morphimY A B : A \subset D -> B \subset D -> f @* (A <*> B) = f @* A <*> f @* B.
proof: Proof. by move=> sAD sBD; rewrite morphim_gen ?morphimU // subUset sAD. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)