:: deftheorem dufe defines unionExt FIELD_12:def 23 :
for F being Field
for E being FieldExtension of F
for L being b₁ -monomorphic Field
for f being Monomorphism of F,L
for S being non empty ascending Subset of (Ext_Set (f,E))
for b₆ being Function of (unionField (S,f,E)),L holds
( b₆ = unionExt (S,f,E) iff for p being Element of S holds b₆ | the carrier of (p `1) = p `2 );