theorem Th7: :: GLIB_000:7

for GS being GraphStruct
for x being set
for n being Nat holds dom (GS .set (n,x)) = (dom GS) \/ {n}