:: deftheorem defines unionCarrier FIELD_12:def 17 :
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 Subset of (Ext_Set (f,E)) holds unionCarrier (S,f,E) = union { the carrier of (p `1) where p is Element of S : verum } ;