:: deftheorem defines union ZF_REFLE:def 1 :
for f being Function
for W being Universe
for a being Ordinal of W holds union (f,a) = Union (W |` (f | (Rank a)));