proposition: Lemma morphimU A B : f @* (A :|: B) = f @* A :|: f @* B.
proof: Proof. by rewrite -imsetU -setIUr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)