theorem Th18: :: LEXBFS:18

for G being _finite _Graph
for S being VNumberingSeq of G
for n being Nat holds S . n is one-to-one