theorem :: FIELD_8:45

for F being Field
for E1 being b₁ -finite FieldExtension of F
for E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
( E2 is F -finite & deg (E1,F) = deg (E2,F) )