let F be non empty Graph-yielding Function; :: thesis: for S being GraphSum of F
for G9 being GraphUnion of rng (canGFDistinction F) holds S is G9 -Disomorphic
let S be GraphSum of F; :: thesis: for G9 being GraphUnion of rng (canGFDistinction F) holds S is G9 -Disomorphic
let G9 be GraphUnion of rng (canGFDistinction F); :: thesis: S is G9 -Disomorphic
consider G8 being GraphUnion of rng (canGFDistinction F) such that
A1: S is G8 -Disomorphic by Def27;
G8 is G9 -Disomorphic by GLIB_014:22, GLIBPRE0:78;
hence S is G9 -Disomorphic by A1; :: thesis: verum