theorem Th39: :: ORDINAL6:39

for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st f is normal & l in dom (criticals f) holds
(criticals f) . l = Union ((criticals f) | l)