theorem :: FIELD_8:42

for F being Field
for E being FieldExtension of F holds E,E are_isomorphic_over F