theorem :: FIELD_7:41

for F being Field
for E being FieldExtension of F holds F_Alg E is FieldExtension of F ;