theorem Th8: :: GLIB_000:8

for GS being GraphStruct
for x being set
for n being Nat holds (GS .set (n,x)) . n = x