:: deftheorem dFA defines FieldAdjunction FIELD_6:def 6 :
for F being Field
for E being FieldExtension of F
for T being Subset of E
for b₄ being strict doubleLoopStr holds
( b₄ = FieldAdjunction (F,T) iff ( the carrier of b₄ = carrierFA T & the addF of b₄ = the addF of E || (carrierFA T) & the multF of b₄ = the multF of E || (carrierFA T) & the OneF of b₄ = 1. E & the ZeroF of b₄ = 0. E ) );