proposition: Lemma morphimP : reflect morphim_spec (y \in f @: (D :&: A)).
proof: Proof. apply: (iffP imsetP) => [] [z]; first by case/setIP; exists z. by exists z; first apply/setIP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)