theorem Th24: :: CLASSES2:24

for L being Sequence st dom L is limit_ordinal & ( for A being Ordinal st A in dom L holds
L . A = Rank A ) holds
Rank (dom L) = Union L