theorem :: GLIB_015:119

for F being non empty Graph-yielding Function
for S1, S2 being GraphSum of F holds S2 is S1 -Disomorphic by Th117;