proposition: Lemma limgE phi : limg phi = vsof e (mxof e e phi).
proof: Proof. apply/vspaceP => v; rewrite -rowmxof_sub//. apply/memv_imgP/submxP => [[u _ ->]|[u /(canRL (rowmxofK _)) ->//]]. by exists (rowmxof e u); rewrite -rowmxof_app. by exists (vecof e u); rewrite ?memvf// -hom_vecof. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)