theorem :: FIELD_8:37

for F being Field
for E being FieldExtension of F
for E1, E2 being b₂ -extending FieldExtension of F
for h being Function of E1,E2 st h is E -fixing holds
h is F -fixing