for a being Ordinal
for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds Union f in U