theorem Th8: :: ZF_REFLE:8

for L being Sequence
for A being Ordinal holds L | (Rank A) is Sequence