theorem fixr: :: FIELD_13:44

for F being Field
for E being b₁ -algebraic FieldExtension of F
for h being b₁ -fixing Monomorphism of E holds the carrier of E c= rng h