let F be Field; :: thesis: for E being F -finite FieldExtension of F holds
( E is F -normal iff ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p )
let E be F -finite FieldExtension of F; :: thesis: ( E is F -normal iff ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p )

now :: thesis: ( ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p implies E is F -normal )

assume ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p ; :: thesis: E is F -normal
then for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E by lemNor2;
hence E is F -normal by lemNor3; :: thesis: verum

end;

hence ( E is F -normal iff ex p being non constant Element of the carrier of (Polynom-Ring F) st E is SplittingField of p ) by lemNor1; :: thesis: verum