proposition: Lemma normalField_isom : {f : {morphism ('Gal(E / K) / 'Gal(E / M)) >-> gal_of M} | isom ('Gal(E / K) / 'Gal (E / M)) 'Gal(M / K) f & (forall A, f @* (A / 'Gal(E / M)) = normalField_cast @* A) /\ {in 'Gal(E / K) & M, forall x, f (coset 'Gal (E / M) x) =1 x} }%g.
proof: Proof. have:= first_isom normalField_cast_morphism; rewrite normalField_ker. case=> f injf Df; exists f; first by apply/isomP; rewrite Df normalField_img. split=> [//|x a galEx /normalField_cast_eq<- //]; congr ((_ : gal_of M) a). apply: set1_inj; rewrite -!morphim_set1 ?mem_quotient ?Df //. by rewrite (subsetP (normal_norm normalField_normal)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)