proposition: Lemma subset_limgP (F0 : fieldType) (L L' : fieldExtType F0) (E : {subfield L}) (f : 'AHom(L, L')) (r' : seq L') : {subset r' <= (f @: E)%VS} <-> (exists2 r, all (mem E) r & r' = map f r).
proof: Proof. split => [|[r /allP/= rE ->] _ /mapP[x xr ->]]; last by rewrite memv_img ?rE. move=> /(_ _ _)/memv_imgP/sig2_eqW-/(all_sig_cond (0 : L))[f' f'P]. exists (map f' r'); first by apply/allP => _ /mapP [x /f'P[? ?] ->]. by symmetry; rewrite -map_comp; apply: map_id_in => x /f'P[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)