:: deftheorem defines -normal FIELD_13:def 5 :
for F being Field
for E being FieldExtension of F holds
( E is F -normal iff ( E is F -algebraic & ( for p being irreducible Element of the carrier of (Polynom-Ring F) st p is_with_roots_in E holds
p splits_in E ) ) );