let F be Field; :: thesis: for E being F -finite FieldExtension of F holds
( E is F -normal iff for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E )
let E be F -finite FieldExtension of F; :: thesis: ( E is F -normal iff for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E )

now :: thesis: ( E is F -normal implies for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E )

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

end;

hence ( E is F -normal iff for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E ) by lemNor3; :: thesis: verum