theorem Th116: :: GLIB_015:116

for F being non empty Graph-yielding Function
for S being GraphSum of F
for G9 being GraphUnion of rng (canGFDistinction F) holds S is G9 -Disomorphic