let S1, S2 be vertex-disjoint GraphUnionSet; :: thesis:
let G1 be GraphUnion of S1; :: thesis:
let G2 be GraphUnion of S2; :: thesis:
assume S1,S2 are_Disomorphic ; :: thesis:
then consider h being one-to-one Function such that
A1: ( dom h = S1 & rng h = S2 ) and
A2: for G being _Graph st G in S1 holds
h . G is b₁ -Disomorphic _Graph ;
h is S1 -defined by A1, RELAT_1:def 18;
then reconsider h = h as ManySortedSet of S1 by A1, PARTFUN1:def 2;
for x being object st x in dom h holds
h . x is _Graph by A2;
then reconsider h = h as Graph-yielding ManySortedSet of S1 by GLIB_000:def 53;
defpred S₁[ object , object ] means ex G being Element of S1 ex F being PGraphMapping of G,h . G st
( $1 = G & $2 = F & F is Disomorphism );
A3: for G being Element of S1 ex F being object st S₁[G,F]

proof

let G be Element of S1; :: thesis:
h . G is G -Disomorphic by A2;
then consider F being PGraphMapping of G,h . G such that
A4: F is Disomorphism by GLIB_010:def 24;
take F ; :: thesis:
take G ; :: thesis:
take F ; :: thesis:
thus ( G = G & F = F & F is Disomorphism ) by A4; :: thesis:

end;

consider H being ManySortedSet of S1 such that
A5: for G being Element of S1 holds S₁[G,H . G] from PBOOLE:sch 6(A3);
A6: for G being Element of S1 ex F being PGraphMapping of G,h . G st
( H . G = F & F is Disomorphism )

proof

let G be Element of S1; :: thesis:
consider G9 being Element of S1, F being PGraphMapping of G9,h . G9 such that
A7: ( G = G9 & H . G = F & F is Disomorphism ) by A5;
thus ex F being PGraphMapping of G,h . G st
( H . G = F & F is Disomorphism ) by A7; :: thesis:

end;

set V = rng (pr1 H);
set E = rng (pr2 H);
for y being object st y in rng (pr1 H) holds
y is Function

proof

let y be object ; :: thesis:
assume y in rng (pr1 H) ; :: thesis:
then consider x being object such that
A8: ( x in dom (pr1 H) & (pr1 H) . x = y ) by FUNCT_1:def 3;
A9: x in dom H by A8, MCART_1:def 12;
then reconsider x = x as Element of S1 ;
consider F being PGraphMapping of x,h . x such that
A10: ( H . x = F & F is Disomorphism ) by A6;
y = F _V by A8, A9, A10, MCART_1:def 12;
hence y is Function ; :: thesis:

end;

then reconsider V = rng (pr1 H) as functional set by FUNCT_1:def 13;
for f1, f2 being Function st f1 in V & f2 in V holds
f1 tolerates f2

proof

let f1, f2 be Function; :: thesis:
assume A11: ( f1 in V & f2 in V ) ; :: thesis:
then consider x1 being object such that
A12: ( x1 in dom (pr1 H) & (pr1 H) . x1 = f1 ) by FUNCT_1:def 3;
A13: x1 in dom H by A12, MCART_1:def 12;
then reconsider x1 = x1 as Element of S1 ;
consider F1 being PGraphMapping of x1,h . x1 such that
A14: ( H . x1 = F1 & F1 is Disomorphism ) by A6;
A15: f1 = F1 _V by A12, A13, A14, MCART_1:def 12;
then A16: dom f1 = the_Vertices_of x1 by A14, GLIB_010:def 11;
consider x2 being object such that
A17: ( x2 in dom (pr1 H) & (pr1 H) . x2 = f2 ) by A11, FUNCT_1:def 3;
A18: x2 in dom H by A17, MCART_1:def 12;
then reconsider x2 = x2 as Element of S1 ;
consider F2 being PGraphMapping of x2,h . x2 such that
A19: ( H . x2 = F2 & F2 is Disomorphism ) by A6;
A20: f2 = F2 _V by A17, A18, A19, MCART_1:def 12;
then A21: dom f2 = the_Vertices_of x2 by A19, GLIB_010:def 11;

per cases ;

suppose x1 = x2 ; :: thesis:

then F1 = F2 by A14, A19;
hence f1 tolerates f2 by A15, A20; :: thesis:

end;

suppose x1 <> x2 ; :: thesis:

then dom f1 misses dom f2 by A16, A21, Def18;
hence f1 tolerates f2 by PARTFUN1:56; :: thesis:

end;

then reconsider V = V as functional compatible set by COMPUT_1:def 1;
for y being object st y in rng (pr2 H) holds
y is Function

proof

let y be object ; :: thesis:
assume y in rng (pr2 H) ; :: thesis:
then consider x being object such that
A22: ( x in dom (pr2 H) & (pr2 H) . x = y ) by FUNCT_1:def 3;
A23: x in dom H by A22, MCART_1:def 13;
then reconsider x = x as Element of S1 ;
consider F being PGraphMapping of x,h . x such that
A24: ( H . x = F & F is Disomorphism ) by A6;
y = F _E by A22, A23, A24, MCART_1:def 13;
hence y is Function ; :: thesis:

end;

then reconsider E = rng (pr2 H) as functional set by FUNCT_1:def 13;
for g1, g2 being Function st g1 in E & g2 in E holds
g1 tolerates g2

proof

let f1, f2 be Function; :: thesis:
assume A25: ( f1 in E & f2 in E ) ; :: thesis:
then consider x1 being object such that
A26: ( x1 in dom (pr2 H) & (pr2 H) . x1 = f1 ) by FUNCT_1:def 3;
A27: x1 in dom H by A26, MCART_1:def 13;
then reconsider x1 = x1 as Element of S1 ;
consider F1 being PGraphMapping of x1,h . x1 such that
A28: ( H . x1 = F1 & F1 is Disomorphism ) by A6;
A29: f1 = F1 _E by A26, A27, A28, MCART_1:def 13;
then A30: dom f1 = the_Edges_of x1 by A28, GLIB_010:def 11;
consider x2 being object such that
A31: ( x2 in dom (pr2 H) & (pr2 H) . x2 = f2 ) by A25, FUNCT_1:def 3;
A32: x2 in dom H by A31, MCART_1:def 13;
then reconsider x2 = x2 as Element of S1 ;
consider F2 being PGraphMapping of x2,h . x2 such that
A33: ( H . x2 = F2 & F2 is Disomorphism ) by A6;
A34: f2 = F2 _E by A31, A32, A33, MCART_1:def 13;
then A35: dom f2 = the_Edges_of x2 by A33, GLIB_010:def 11;

per cases ;

suppose x1 = x2 ; :: thesis:

then F1 = F2 by A28, A33;
hence f1 tolerates f2 by A29, A34; :: thesis:

end;

suppose x1 <> x2 ; :: thesis:

then dom f1 misses dom f2 by A30, A35, Def19;
hence f1 tolerates f2 by PARTFUN1:56; :: thesis:

end;

then reconsider E = E as functional compatible set by COMPUT_1:def 1;
set f = union V;
set g = union E;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom (union V) ; :: thesis:
then [x,((union V) . x)] in union V by FUNCT_1:1;
then consider y being set such that
A36: ( [x,((union V) . x)] in y & y in V ) by TARSKI:def 4;
consider z being object such that
A37: ( z in dom (pr1 H) & (pr1 H) . z = y ) by A36, FUNCT_1:def 3;
A38: z in dom H by A37, MCART_1:def 12;
then reconsider z = z as Element of S1 ;
take Y = the_Vertices_of z; :: thesis:
consider F being PGraphMapping of z,h . z such that
A39: ( H . z = F & F is Disomorphism ) by A6;
y = F _V by A37, A38, A39, MCART_1:def 12;
then x in dom (F _V) by A36, FUNCT_1:1;
hence x in Y ; :: thesis:
thus Y in the_Vertices_of S1 by GLIB_014:def 14; :: thesis:

end;

given Y being set such that A40: ( x in Y & Y in the_Vertices_of S1 ) ; :: thesis:
consider z being _Graph such that
A41: ( z in S1 & Y = the_Vertices_of z ) by A40, GLIB_014:def 14;
reconsider z = z as Element of S1 by A41;
consider F being PGraphMapping of z,h . z such that
A42: ( H . z = F & F is Disomorphism ) by A6;
A43: z in dom H by A41, PARTFUN1:def 2;
x in dom (F _V) by A40, A41, A42, GLIB_010:def 11;
then [x,((F _V) . x)] in F _V by FUNCT_1:1;
then A44: [x,((F _V) . x)] in (pr1 H) . z by A42, A43, MCART_1:def 12;
z in dom (pr1 H) by A43, MCART_1:def 12;
then (pr1 H) . z in rng (pr1 H) by FUNCT_1:3;
then [x,((F _V) . x)] in union V by A44, TARSKI:def 4;
hence x in dom (union V) by FUNCT_1:1; :: thesis:

end;

then A45: dom (union V) = union (the_Vertices_of S1) by TARSKI:def 4
.= the_Vertices_of G1 by GLIB_014:def 25 ;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng (union V) ; :: thesis:
then consider x being object such that
A46: ( x in dom (union V) & (union V) . x = y ) by FUNCT_1:def 3;
[x,y] in union V by A46, FUNCT_1:1;
then consider Z being set such that
A47: ( [x,y] in Z & Z in V ) by TARSKI:def 4;
consider z being object such that
A48: ( z in dom (pr1 H) & (pr1 H) . z = Z ) by A47, FUNCT_1:def 3;
A49: z in dom H by A48, MCART_1:def 12;
then reconsider z = z as Element of S1 ;
h . z in rng h by A1, FUNCT_1:3;
then reconsider G = h . z as Element of S2 by A1;
consider F being PGraphMapping of z,G such that
A50: ( H . z = F & F is Disomorphism ) by A6;
take Y = the_Vertices_of G; :: thesis:
Z = F _V by A48, A49, A50, MCART_1:def 12;
then y in rng (F _V) by A47, XTUPLE_0:def 13;
hence y in Y ; :: thesis:
thus Y in the_Vertices_of S2 by GLIB_014:def 14; :: thesis:

end;

given Y being set such that A51: ( y in Y & Y in the_Vertices_of S2 ) ; :: thesis:
consider G being _Graph such that
A52: ( G in S2 & Y = the_Vertices_of G ) by A51, GLIB_014:def 14;
consider z being object such that
A53: ( z in dom h & h . z = G ) by A1, A52, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A53;
consider F being PGraphMapping of z,G such that
A54: ( H . z = F & F is Disomorphism ) by A6, A53;
y in rng (F _V) by A51, A52, A54, GLIB_010:def 12;
then consider x being object such that
A55: ( x in dom (F _V) & (F _V) . x = y ) by FUNCT_1:def 3;
z in S1 ;
then A56: z in dom H by PARTFUN1:def 2;
A57: F _V = (pr1 H) . z by A54, A56, MCART_1:def 12;
z in dom (pr1 H) by A56, MCART_1:def 12;
then A58: (pr1 H) . z in rng (pr1 H) by FUNCT_1:3;
[x,y] in (pr1 H) . z by A55, A57, FUNCT_1:1;
then [x,y] in union V by A58, TARSKI:def 4;
hence y in rng (union V) by XTUPLE_0:def 13; :: thesis:

end;

then A59: rng (union V) = union (the_Vertices_of S2) by TARSKI:def 4
.= the_Vertices_of G2 by GLIB_014:def 25 ;
then reconsider f = union V as Function of (the_Vertices_of G1),(the_Vertices_of G2) by A45, FUNCT_2:1;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom (union E) ; :: thesis:
then [x,((union E) . x)] in union E by FUNCT_1:1;
then consider y being set such that
A60: ( [x,((union E) . x)] in y & y in E ) by TARSKI:def 4;
consider z being object such that
A61: ( z in dom (pr2 H) & (pr2 H) . z = y ) by A60, FUNCT_1:def 3;
A62: z in dom H by A61, MCART_1:def 13;
then reconsider z = z as Element of S1 ;
take Y = the_Edges_of z; :: thesis:
consider F being PGraphMapping of z,h . z such that
A63: ( H . z = F & F is Disomorphism ) by A6;
y = F _E by A61, A62, A63, MCART_1:def 13;
then x in dom (F _E) by A60, FUNCT_1:1;
hence x in Y ; :: thesis:
thus Y in the_Edges_of S1 by GLIB_014:def 15; :: thesis:

end;

given Y being set such that A64: ( x in Y & Y in the_Edges_of S1 ) ; :: thesis:
consider z being _Graph such that
A65: ( z in S1 & Y = the_Edges_of z ) by A64, GLIB_014:def 15;
reconsider z = z as Element of S1 by A65;
consider F being PGraphMapping of z,h . z such that
A66: ( H . z = F & F is Disomorphism ) by A6;
A67: z in dom H by A65, PARTFUN1:def 2;
x in dom (F _E) by A64, A65, A66, GLIB_010:def 11;
then [x,((F _E) . x)] in F _E by FUNCT_1:1;
then A68: [x,((F _E) . x)] in (pr2 H) . z by A66, A67, MCART_1:def 13;
z in dom (pr2 H) by A67, MCART_1:def 13;
then (pr2 H) . z in rng (pr2 H) by FUNCT_1:3;
then [x,((F _E) . x)] in union E by A68, TARSKI:def 4;
hence x in dom (union E) by FUNCT_1:1; :: thesis:

end;

then A69: dom (union E) = union (the_Edges_of S1) by TARSKI:def 4
.= the_Edges_of G1 by GLIB_014:def 25 ;

now :: thesis:

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng (union E) ; :: thesis:
then consider x being object such that
A70: ( x in dom (union E) & (union E) . x = y ) by FUNCT_1:def 3;
[x,y] in union E by A70, FUNCT_1:1;
then consider Z being set such that
A71: ( [x,y] in Z & Z in E ) by TARSKI:def 4;
consider z being object such that
A72: ( z in dom (pr2 H) & (pr2 H) . z = Z ) by A71, FUNCT_1:def 3;
A73: z in dom H by A72, MCART_1:def 13;
then reconsider z = z as Element of S1 ;
h . z in rng h by A1, FUNCT_1:3;
then reconsider G = h . z as Element of S2 by A1;
consider F being PGraphMapping of z,G such that
A74: ( H . z = F & F is Disomorphism ) by A6;
take Y = the_Edges_of G; :: thesis:
Z = F _E by A72, A73, A74, MCART_1:def 13;
then y in rng (F _E) by A71, XTUPLE_0:def 13;
hence y in Y ; :: thesis:
thus Y in the_Edges_of S2 by GLIB_014:def 15; :: thesis:

end;

given Y being set such that A75: ( y in Y & Y in the_Edges_of S2 ) ; :: thesis:
consider G being _Graph such that
A76: ( G in S2 & Y = the_Edges_of G ) by A75, GLIB_014:def 15;
consider z being object such that
A77: ( z in dom h & h . z = G ) by A1, A76, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A77;
consider F being PGraphMapping of z,G such that
A78: ( H . z = F & F is Disomorphism ) by A6, A77;
y in rng (F _E) by A75, A76, A78, GLIB_010:def 12;
then consider x being object such that
A79: ( x in dom (F _E) & (F _E) . x = y ) by FUNCT_1:def 3;
z in S1 ;
then A80: z in dom H by PARTFUN1:def 2;
A81: F _E = (pr2 H) . z by A78, A80, MCART_1:def 13;
z in dom (pr2 H) by A80, MCART_1:def 13;
then A82: (pr2 H) . z in rng (pr2 H) by FUNCT_1:3;
[x,y] in (pr2 H) . z by A79, A81, FUNCT_1:1;
then [x,y] in union E by A82, TARSKI:def 4;
hence y in rng (union E) by XTUPLE_0:def 13; :: thesis:

end;

then A83: rng (union E) = union (the_Edges_of S2) by TARSKI:def 4
.= the_Edges_of G2 by GLIB_014:def 25 ;
then reconsider g = union E as Function of (the_Edges_of G1),(the_Edges_of G2) by A69, FUNCT_2:1;

now :: thesis:

let f1 be Function; :: thesis:
assume f1 in V ; :: thesis:
then consider z1 being object such that
A84: ( z1 in dom (pr1 H) & (pr1 H) . z1 = f1 ) by FUNCT_1:def 3;
A85: z1 in dom H by A84, MCART_1:def 12;
then reconsider z1 = z1 as Element of S1 ;
consider F1 being PGraphMapping of z1,h . z1 such that
A86: ( H . z1 = F1 & F1 is Disomorphism ) by A6;
A87: f1 = F1 _V by A84, A85, A86, MCART_1:def 12;
hence f1 is one-to-one by A86; :: thesis:
let f2 be Function; :: thesis:
assume A88: ( f2 in V & f1 <> f2 ) ; :: thesis:
then consider z2 being object such that
A89: ( z2 in dom (pr1 H) & (pr1 H) . z2 = f2 ) by FUNCT_1:def 3;
A90: z2 in dom H by A89, MCART_1:def 12;
then reconsider z2 = z2 as Element of S1 ;
consider F2 being PGraphMapping of z2,h . z2 such that
A91: ( H . z2 = F2 & F2 is Disomorphism ) by A6;
A92: f2 = F2 _V by A89, A90, A91, MCART_1:def 12;
then z1 <> z2 by A86, A87, A88, A91;
then A93: h . z1 <> h . z2 by A1, FUNCT_1:def 4;
( h . z1 in S2 & h . z2 in S2 ) by A1, FUNCT_1:3;
then the_Vertices_of (h . z1) misses the_Vertices_of (h . z2) by A93, Def18;
then rng (F1 _V) misses the_Vertices_of (h . z2) by A86, GLIB_010:def 12;
hence rng f1 misses rng f2 by A87, A91, A92, GLIB_010:def 12; :: thesis:

end;

then A94: f is one-to-one by GLIBPRE1:16;

now :: thesis:

let g1 be Function; :: thesis:
assume g1 in E ; :: thesis:
then consider z1 being object such that
A95: ( z1 in dom (pr2 H) & (pr2 H) . z1 = g1 ) by FUNCT_1:def 3;
A96: z1 in dom H by A95, MCART_1:def 13;
then reconsider z1 = z1 as Element of S1 ;
consider F1 being PGraphMapping of z1,h . z1 such that
A97: ( H . z1 = F1 & F1 is Disomorphism ) by A6;
A98: g1 = F1 _E by A95, A96, A97, MCART_1:def 13;
hence g1 is one-to-one by A97; :: thesis:
let g2 be Function; :: thesis:
assume A99: ( g2 in E & g1 <> g2 ) ; :: thesis:
then consider z2 being object such that
A100: ( z2 in dom (pr2 H) & (pr2 H) . z2 = g2 ) by FUNCT_1:def 3;
A101: z2 in dom H by A100, MCART_1:def 13;
then reconsider z2 = z2 as Element of S1 ;
consider F2 being PGraphMapping of z2,h . z2 such that
A102: ( H . z2 = F2 & F2 is Disomorphism ) by A6;
A103: g2 = F2 _E by A100, A101, A102, MCART_1:def 13;
then z1 <> z2 by A97, A98, A99, A102;
then A104: h . z1 <> h . z2 by A1, FUNCT_1:def 4;
( h . z1 in S2 & h . z2 in S2 ) by A1, FUNCT_1:3;
then the_Edges_of (h . z1) misses the_Edges_of (h . z2) by A104, Def19;
then rng (F1 _E) misses the_Edges_of (h . z2) by A97, GLIB_010:def 12;
hence rng g1 misses rng g2 by A98, A102, A103, GLIB_010:def 12; :: thesis:

end;

then A105: g is one-to-one by GLIBPRE1:16;

now :: thesis:

hereby :: thesis:

let e be object ; :: thesis:
assume e in dom g ; :: thesis:
then [e,(g . e)] in g by FUNCT_1:1;
then consider Y being set such that
A106: ( [e,(g . e)] in Y & Y in E ) by TARSKI:def 4;
consider z being object such that
A107: ( z in dom (pr2 H) & (pr2 H) . z = Y ) by A106, FUNCT_1:def 3;
A108: z in dom H by A107, MCART_1:def 13;
then reconsider z = z as Element of S1 ;
consider F being PGraphMapping of z,h . z such that
A109: ( H . z = F & F is Disomorphism ) by A6;
Y = F _E by A107, A108, A109, MCART_1:def 13;
then A110: e in dom (F _E) by A106, FUNCT_1:1;
then A111: ( (the_Source_of z) . e in dom (F _V) & (the_Target_of z) . e in dom (F _V) ) by GLIB_010:5;
A112: ( e in the_Edges_of z & e is set ) by A110;
set v = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
z is Subgraph of G1 by GLIB_014:21;
then A113: ( (the_Source_of G1) . e in dom (F _V) & (the_Target_of G1) . e in dom (F _V) ) by A111, A112, GLIB_000:def 32;
A114: F _V = (pr1 H) . z by A108, A109, MCART_1:def 12;
z in dom (pr1 H) by A108, MCART_1:def 12;
then A115: F _V in V by A114, FUNCT_1:def 3;
( [((the_Source_of G1) . e),((F _V) . ((the_Source_of G1) . e))] in F _V & [((the_Target_of G1) . e),((F _V) . ((the_Target_of G1) . e))] in F _V ) by A113, FUNCT_1:1;
then ( [((the_Source_of G1) . e),((F _V) . ((the_Source_of G1) . e))] in f & [((the_Target_of G1) . e),((F _V) . ((the_Target_of G1) . e))] in f ) by A115, TARSKI:def 4;
hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by FUNCT_1:1; :: thesis:

end;

let e, v, w be object ; :: thesis:
assume ( e in dom g & v in dom f & w in dom f ) ; :: thesis:
assume e DJoins v,w,G1 ; :: thesis:
then consider z being Element of S1 such that
A116: e DJoins v,w,z by GLIBPRE1:116;
consider F being PGraphMapping of z,h . z such that
A117: ( H . z = F & F is Disomorphism ) by A6;
e in the_Edges_of z by A116, GLIB_000:def 14;
then A118: e in dom (F _E) by A117, GLIB_010:def 11;
e Joins v,w,z by A116, GLIB_000:16;
then ( v in the_Vertices_of z & w in the_Vertices_of z ) by GLIB_000:13;
then A119: ( v in dom (F _V) & w in dom (F _V) ) by A117, GLIB_010:def 11;
then A120: (F _E) . e DJoins (F _V) . v,(F _V) . w,h . z by A116, A117, A118, GLIB_010:def 14;
h . z in S2 by A1, FUNCT_1:3;
then A121: h . z is Subgraph of G2 by GLIB_014:21;
A122: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A120, A121, GLIB_000:72;
z in S1 ;
then A123: z in dom H by PARTFUN1:def 2;
then z in dom (pr1 H) by MCART_1:def 12;
then A124: (pr1 H) . z in V by FUNCT_1:3;
z in dom (pr2 H) by A123, MCART_1:def 13;
then A125: (pr2 H) . z in E by FUNCT_1:3;
F _V = (pr1 H) . z by A117, A123, MCART_1:def 12;
then A126: ( (F _V) . v = f . v & (F _V) . w = f . w ) by A119, A124, COMPUT_1:13;
F _E = (pr2 H) . z by A117, A123, MCART_1:def 13;
then (F _E) . e = g . e by A118, A125, COMPUT_1:13;
hence g . e DJoins f . v,f . w,G2 by A126, A122; :: thesis:

end;

then reconsider F = [f,g] as directed PGraphMapping of G1,G2 by GLIB_010:30;
( F _V = f & F _E = g ) ;
then A127: F is one-to-one by A94, A105, GLIB_010:def 13;
( F _V = f & F _E = g ) ;
then ( F is total & F is onto ) by A45, A59, A69, A83, GLIB_010:def 11, GLIB_010:def 12;
hence G2 is G1 -Disomorphic by A127, GLIB_010:def 24; :: thesis: