theorem iso: :: FIELD_13:45

for F being Field
for E being b₁ -algebraic FieldExtension of F
for h being b₁ -fixing Monomorphism of E holds h is Automorphism of E