theorem :: FIELD_7:42

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