theorem Th21: :: LEXBFS:21

for G being _finite _Graph
for S being VNumberingSeq of G
for m, n being Nat st n < S .Lifespan() & n < m holds
( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n )