:: deftheorem defemb defines embField FIELD_2:def 7 :
for K being Field
for T being b₁ -monomorphic comRing
for f being Monomorphism of K,T
for b₄ being strict doubleLoopStr holds
( b₄ = embField f iff ( the carrier of b₄ = carr f & the addF of b₄ = addemb f & the multF of b₄ = multemb f & the OneF of b₄ = 1. K & the ZeroF of b₄ = 0. K ) );