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