:: deftheorem d defines Field_of_Algebraic_Elements FIELD_7:def 14 :
for F being Field
for E being FieldExtension of F
for b₃ being strict doubleLoopStr holds
( b₃ = Field_of_Algebraic_Elements E iff ( the carrier of b₃ = Alg_El E & the addF of b₃ = the addF of E || the carrier of b₃ & the multF of b₃ = the multF of E || the carrier of b₃ & the OneF of b₃ = 1. E & the ZeroF of b₃ = 0. E ) );