theorem Th14: :: ZF_REFLE:14

for W being Universe
for a being Ordinal of W
for phi being Ordinal-Sequence of W holds
( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) )