proposition: Lemma morphimD A B : f @* A :\: f @* B \subset f @* (A :\: B).
proof: Proof. rewrite subDset -morphimU morphimS //. by rewrite setDE setUIr setUCr setIT subsetUr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)