:: deftheorem defiso defines emb_iso FIELD_2:def 8 :
for K being Field
for F being b₁ -monomorphic Field
for f being Monomorphism of K,F
for b₄ being Function of (embField f),F holds
( b₄ = emb_iso f iff ( ( for a being Element of (embField f) st not a in K holds
b₄ . a = a ) & ( for a being Element of (embField f) st a in K holds
b₄ . a = f . a ) ) );