proposition: Lemma restrmEsub B : B \subset A -> fA @* B = f @* B.
proof: Proof. by rewrite morphim_restrm => /setIidPr->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)