theorem :: FIELD_7:44

for F being Field
for E being b₁ -algebraic FieldExtension of F holds F_Alg E == E