theorem :: FIELD_7:44
for F being Field
for E being b1 -algebraic FieldExtension of F holds F_Alg E == E