theorem Th16: :: ZF_REFLE:16

for W being Universe
for a being Ordinal of W
for L being DOMAIN-Sequence of W holds L . a c= Union L