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