let F1, F2 be non empty Graph-yielding Function; :: thesis: for S1 being GraphSum of F1
for S2 being GraphSum of F2 st F1,F2 are_Disomorphic holds
S2 is S1 -Disomorphic
let S1 be GraphSum of F1; :: thesis: for S2 being GraphSum of F2 st F1,F2 are_Disomorphic holds
S2 is S1 -Disomorphic
let S2 be GraphSum of F2; :: thesis: ( F1,F2 are_Disomorphic implies S2 is S1 -Disomorphic )
set C1 = canGFDistinction F1;
set C2 = canGFDistinction F2;
set T1 = the GraphUnion of rng (canGFDistinction F1);
set T2 = the GraphUnion of rng (canGFDistinction F2);
assume F1,F2 are_Disomorphic ; :: thesis: S2 is S1 -Disomorphic
then rng (canGFDistinction F1), rng (canGFDistinction F2) are_Disomorphic by Th74, Th88;
then A1: the GraphUnion of rng (canGFDistinction F2) is the GraphUnion of rng (canGFDistinction F1) -Disomorphic by Th55;
A2: ( S1 is the GraphUnion of rng (canGFDistinction F1) -Disomorphic & S2 is the GraphUnion of rng (canGFDistinction F2) -Disomorphic ) by Th116;
then the GraphUnion of rng (canGFDistinction F1) is S1 -Disomorphic by GLIB_010:96;
hence S2 is S1 -Disomorphic by A1, A2; :: thesis: verum