:: deftheorem dua defines unionAdd FIELD_12:def 18 :
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 BinOp of (unionCarrier (S,f,E)) holds
( b₆ = unionAdd (S,f,E) iff for a, b being Element of unionCarrier (S,f,E) ex p being Element of S ex x, y being Element of (p `1) st
( x = a & y = b & b₆ . (a,b) = x + y ) );