:: deftheorem defzero defines unionZero FIELD_12:def 21 :
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 Element of unionCarrier (S,f,E) holds
( b₆ = unionZero (S,f,E) iff ex p being Element of S st b₆ = 0. (p `1) );