let S1, S2 be vertex-disjoint GraphUnionSet; :: thesis: for G1 being GraphUnion of S1
for G2 being GraphUnion of S2 st S1,S2 are_isomorphic holds
G2 is G1 -isomorphic
let G1 be GraphUnion of S1; :: thesis: for G2 being GraphUnion of S2 st S1,S2 are_isomorphic holds
G2 is G1 -isomorphic
let G2 be GraphUnion of S2; :: thesis: ( S1,S2 are_isomorphic implies G2 is G1 -isomorphic )
assume S1,S2 are_isomorphic ; :: thesis: G2 is G1 -isomorphic
then consider S3 being vertex-disjoint GraphUnionSet, E being Subset of (the_Edges_of G2), G3 being GraphUnion of S3 such that
A1: S1,S3 are_Disomorphic and
A2: G3 is reverseEdgeDirections of G2,E by Th56;
A3: G3 is G1 -Disomorphic by A1, Th55;
G3 is G2 -isomorphic by A2, GLIBPRE0:80;
then G2 is G3 -isomorphic by GLIB_010:95;
hence G2 is G1 -isomorphic by A3; :: thesis: verum