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_isomorphic holds
S2 is S1 -isomorphic
let S1 be GraphSum of F1; :: thesis: for S2 being GraphSum of F2 st F1,F2 are_isomorphic holds
S2 is S1 -isomorphic
let S2 be GraphSum of F2; :: thesis: ( F1,F2 are_isomorphic implies S2 is S1 -isomorphic )
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_isomorphic ; :: thesis: S2 is S1 -isomorphic
then canGFDistinction F1, canGFDistinction F2 are_isomorphic by Th89;
then A1: the GraphUnion of rng (canGFDistinction F2) is the GraphUnion of rng (canGFDistinction F1) -isomorphic by Th57, Th75;
A2: ( S1 is the GraphUnion of rng (canGFDistinction F1) -Disomorphic & S2 is the GraphUnion of rng (canGFDistinction F2) -Disomorphic ) by Th116;
then S1 is the GraphUnion of rng (canGFDistinction F1) -isomorphic ;
then the GraphUnion of rng (canGFDistinction F1) is S1 -isomorphic by GLIB_010:95;
hence S2 is S1 -isomorphic by A1, A2; :: thesis: verum