theorem Th117: :: GLIB_015:117

for F1, F2 being non empty Graph-yielding Function
for S1 being GraphSum of F1
for S2 being GraphSum of F2 st F1,F2 are_Disomorphic holds
S2 is S1 -Disomorphic