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_isomorphic ; :: 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₁ -isomorphic _Graph ;
reconsider h = h as ManySortedSet of S1 by A1, RELAT_1:def 18, 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 isomorphism );
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 -isomorphic by A2;
then consider F being PGraphMapping of G,h . G such that
A4: F is isomorphism by GLIB_010:def 23;
take F ; :: thesis:
take G ; :: thesis:
take F ; :: thesis:
thus ( G = G & F = F & F is isomorphism ) 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 isomorphism )

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 isomorphism ) by A5;
thus ex F being PGraphMapping of G,h . G st
( H . G = F & F is isomorphism ) by A7; :: thesis:

end;

defpred S₂[ object , object ] means ex G being Element of S1 ex E being Subset of (the_Edges_of (h . G)) st
( $1 = G & $2 = E & ( for G9 being reverseEdgeDirections of h . G,E ex F being PGraphMapping of G,G9 st
( F = H . G & F is Disomorphism ) ) );
A8: for G being Element of S1 ex E being object st S₂[G,E]

proof

let G be Element of S1; :: thesis:
consider F0 being PGraphMapping of G,h . G such that
A9: ( H . G = F0 & F0 is isomorphism ) by A6;
F0 _E is one-to-one by A9;
then consider E being Subset of (the_Edges_of (h . G)) such that
A10: for G9 being reverseEdgeDirections of h . G,E ex F being PGraphMapping of G,G9 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) by GLIBPRE0:87;
take E ; :: thesis:
take G ; :: thesis:
take E ; :: thesis:
thus ( G = G & E = E ) ; :: thesis:
let G9 be reverseEdgeDirections of h . G,E; :: thesis:
consider F being PGraphMapping of G,G9 such that
A11: ( F = F0 & F is directed ) and
( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) ) and
A12: ( F0 is isomorphism implies F is isomorphism ) by A10;
take F ; :: thesis:
thus ( F = H . G & F is Disomorphism ) by A9, A11, A12; :: thesis:

end;

consider A being ManySortedSet of S1 such that
A13: for G being Element of S1 holds S₂[G,A . G] from PBOOLE:sch 6(A8);
A14: for G being Element of S1 holds A . G is Subset of (the_Edges_of (h . G))

proof

let G be Element of S1; :: thesis:
consider G0 being Element of S1, E0 being Subset of (the_Edges_of (h . G0)) such that
A15: ( G = G0 & A . G = E0 ) and
for G9 being reverseEdgeDirections of h . G0,E0 ex F being PGraphMapping of G0,G9 st
( F = H . G0 & F is Disomorphism ) by A13;
thus A . G is Subset of (the_Edges_of (h . G)) by A15; :: thesis:

end;

A16: for G being Element of S1
for G9 being reverseEdgeDirections of h . G,A . G ex F being PGraphMapping of G,G9 st
( F = H . G & F is Disomorphism )

proof

let G be Element of S1; :: thesis:
consider G0 being Element of S1, E0 being Subset of (the_Edges_of (h . G0)) such that
A17: ( G = G0 & A . G = E0 ) and
A18: for G9 being reverseEdgeDirections of h . G0,E0 ex F being PGraphMapping of G0,G9 st
( F = H . G0 & F is Disomorphism ) by A13;
thus for G9 being reverseEdgeDirections of h . G,A . G ex F being PGraphMapping of G,G9 st
( F = H . G & F is Disomorphism ) by A17, A18; :: thesis:

end;

deffunc H₁( Element of S1) -> reverseEdgeDirections of h . $1,A . $1 = the reverseEdgeDirections of h . $1,A . $1;
consider B being ManySortedSet of S1 such that
A19: for G being Element of S1 holds B . G = H₁(G) from PBOOLE:sch 5();

now :: thesis:

let x be object ; :: thesis:
assume x in dom B ; :: thesis:
then reconsider G = x as Element of S1 ;
B . G = the reverseEdgeDirections of h . G,A . G by A19;
hence B . x is _Graph ; :: thesis:

end;

then reconsider B = B as Graph-yielding ManySortedSet of S1 by GLIB_000:def 53;

now :: thesis:

let x1, x2 be object ; :: thesis:
assume A20: ( x1 in dom B & x2 in dom B & B . x1 = B . x2 ) ; :: thesis:
then reconsider H1 = x1 as Element of S1 ;
reconsider H2 = x2 as Element of S1 by A20;
( H1 in S1 & H2 in S1 ) ;
then A21: ( x1 in dom h & x2 in dom h ) by A1;
then A22: ( h . x1 in S2 & h . x2 in S2 ) by A1, FUNCT_1:3;
B . H1 = the reverseEdgeDirections of h . H1,A . H1 by A19;
then A23: the_Vertices_of (B . H1) = the_Vertices_of (h . H1) by GLIB_007:4;
B . H2 = the reverseEdgeDirections of h . H2,A . H2 by A19;
then the_Vertices_of (h . H1) = the_Vertices_of (h . H2) by A20, A23, GLIB_007:4;
hence x1 = x2 by A21, A22, Def18, FUNCT_1:def 4; :: thesis:

end;

then A24: B is one-to-one by FUNCT_1:def 4;

now :: thesis:

let H3, H4 be _Graph; :: thesis:
assume A25: ( H3 in rng B & H4 in rng B & H3 <> H4 ) ; :: thesis:
then consider H1 being object such that
A26: ( H1 in dom B & B . H1 = H3 ) by FUNCT_1:def 3;
consider H2 being object such that
A27: ( H2 in dom B & B . H2 = H4 ) by A25, FUNCT_1:def 3;
reconsider H1 = H1, H2 = H2 as Element of S1 by A26, A27;
B . H1 = the reverseEdgeDirections of h . H1,A . H1 by A19;
then A28: the_Vertices_of (B . H1) = the_Vertices_of (h . H1) by GLIB_007:4;
B . H2 = the reverseEdgeDirections of h . H2,A . H2 by A19;
then A29: the_Vertices_of (B . H2) = the_Vertices_of (h . H2) by GLIB_007:4;
A30: ( h . H1 in S2 & h . H2 in S2 ) by A1, FUNCT_1:3;
H1 <> H2 by A25, A26, A27;
then h . H1 <> h . H2 by A1, FUNCT_1:def 4;
then the_Vertices_of (h . H1) misses the_Vertices_of (h . H2) by A30, Def18;
hence the_Vertices_of H3 misses the_Vertices_of H4 by A26, A27, A28, A29; :: thesis:

end;

then A31: rng B is vertex-disjoint ;

now :: thesis:

let H3, H4 be _Graph; :: thesis:
assume A32: ( H3 in rng B & H4 in rng B & H3 <> H4 ) ; :: thesis:
then consider H1 being object such that
A33: ( H1 in dom B & B . H1 = H3 ) by FUNCT_1:def 3;
consider H2 being object such that
A34: ( H2 in dom B & B . H2 = H4 ) by A32, FUNCT_1:def 3;
reconsider H1 = H1, H2 = H2 as Element of S1 by A33, A34;
B . H1 = the reverseEdgeDirections of h . H1,A . H1 by A19;
then A35: the_Edges_of (B . H1) = the_Edges_of (h . H1) by GLIB_007:4;
B . H2 = the reverseEdgeDirections of h . H2,A . H2 by A19;
then A36: the_Edges_of (B . H2) = the_Edges_of (h . H2) by GLIB_007:4;
A37: ( h . H1 in S2 & h . H2 in S2 ) by A1, FUNCT_1:3;
H1 <> H2 by A32, A33, A34;
then h . H1 <> h . H2 by A1, FUNCT_1:def 4;
then the_Edges_of (h . H1) misses the_Edges_of (h . H2) by A37, Def19;
hence the_Edges_of H3 misses the_Edges_of H4 by A33, A34, A35, A36; :: thesis:

end;

then A38: rng B is edge-disjoint ;
dom B = S1 by PARTFUN1:def 2;
then not B is empty ;
then reconsider S3 = rng B as vertex-disjoint GraphUnionSet by A31, A38;
for y being object st y in union (rng A) holds
y in the_Edges_of G2

proof

let y be object ; :: thesis:
assume y in union (rng A) ; :: thesis:
then consider Y being set such that
A39: ( y in Y & Y in rng A ) by TARSKI:def 4;
consider x being object such that
A40: ( x in dom A & A . x = Y ) by A39, FUNCT_1:def 3;
reconsider x = x as Element of S1 by A40;
consider G0 being Element of S1, E0 being Subset of (the_Edges_of (h . G0)) such that
A41: ( x = G0 & A . x = E0 ) and
for G9 being reverseEdgeDirections of h . G0,E0 ex F being PGraphMapping of G0,G9 st
( F = H . G0 & F is Disomorphism ) by A13;
y in E0 by A39, A40, A41;
then A42: y in the_Edges_of (h . x) by A41;
h . x in S2 by A1, FUNCT_1:3;
then h . x is Subgraph of G2 by GLIB_014:21;
then the_Edges_of (h . x) c= the_Edges_of G2 by GLIB_000:def 32;
hence y in the_Edges_of G2 by A42; :: thesis:

end;

then reconsider E = union (rng A) as Subset of (the_Edges_of G2) by TARSKI:def 3;
take S3 ; :: thesis:
take E ; :: thesis:
take G3 = the GraphUnion of S3; :: thesis:

now :: thesis:

reconsider f = B as one-to-one Function by A24;
take f = f; :: thesis:
thus ( dom f = S1 & rng f = S3 ) by PARTFUN1:def 2; :: thesis:
let G be _Graph; :: thesis:
assume G in S1 ; :: thesis:
then reconsider G0 = G as Element of S1 ;
B . G0 = the reverseEdgeDirections of h . G0,A . G0 by A19;
then consider F being PGraphMapping of G,B . G0 such that
A43: ( F = H . G0 & F is Disomorphism ) by A16;
thus f . G is G -Disomorphic _Graph by A43, GLIB_010:def 24; :: thesis:

end;

hence S1,S3 are_Disomorphic ; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Vertices_of S2 ; :: thesis:
then consider G being _Graph such that
A44: ( G in S2 & x = the_Vertices_of G ) by GLIB_014:def 14;
consider z being object such that
A45: ( z in dom h & h . z = G ) by A1, A44, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A45;
z in dom B by A1, A45, PARTFUN1:def 2;
then A46: B . z in rng B by FUNCT_1:3;
B . z = the reverseEdgeDirections of h . z,A . z by A19;
then the_Vertices_of (B . z) = x by A44, A45, GLIB_007:4;
hence x in the_Vertices_of (rng B) by A46, GLIB_014:def 14; :: thesis:

end;

assume x in the_Vertices_of (rng B) ; :: thesis:
then consider G being _Graph such that
A47: ( G in rng B & x = the_Vertices_of G ) by GLIB_014:def 14;
consider z being object such that
A48: ( z in dom B & B . z = G ) by A47, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A48;
A49: h . z in S2 by A1, FUNCT_1:3;
B . z = the reverseEdgeDirections of h . z,A . z by A19;
then the_Vertices_of (h . z) = x by A47, A48, GLIB_007:4;
hence x in the_Vertices_of S2 by A49, GLIB_014:def 14; :: thesis:

end;

then A50: the_Vertices_of S2 = the_Vertices_of (rng B) by TARSKI:2;
thus the_Vertices_of G3 = union (the_Vertices_of (rng B)) by GLIB_014:def 25
.= the_Vertices_of G2 by A50, GLIB_014:def 25 ; :: thesis:

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in the_Edges_of S2 ; :: thesis:
then consider G being _Graph such that
A51: ( G in S2 & x = the_Edges_of G ) by GLIB_014:def 15;
consider z being object such that
A52: ( z in dom h & h . z = G ) by A1, A51, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A52;
z in dom B by A1, A52, PARTFUN1:def 2;
then A53: B . z in rng B by FUNCT_1:3;
B . z = the reverseEdgeDirections of h . z,A . z by A19;
then the_Edges_of (B . z) = x by A51, A52, GLIB_007:4;
hence x in the_Edges_of (rng B) by A53, GLIB_014:def 15; :: thesis:

end;

assume x in the_Edges_of (rng B) ; :: thesis:
then consider G being _Graph such that
A54: ( G in rng B & x = the_Edges_of G ) by GLIB_014:def 15;
consider z being object such that
A55: ( z in dom B & B . z = G ) by A54, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A55;
A56: h . z in S2 by A1, FUNCT_1:3;
B . z = the reverseEdgeDirections of h . z,A . z by A19;
then the_Edges_of (h . z) = x by A54, A55, GLIB_007:4;
hence x in the_Edges_of S2 by A56, GLIB_014:def 15; :: thesis:

end;

then A57: the_Edges_of S2 = the_Edges_of (rng B) by TARSKI:2;
thus A58: the_Edges_of G3 = union (the_Edges_of (rng B)) by GLIB_014:def 25
.= the_Edges_of G2 by A57, GLIB_014:def 25 ; :: thesis:
A59: dom (the_Source_of G3) = the_Edges_of G3 by FUNCT_2:def 1
.= (the_Edges_of G2) \/ ((the_Edges_of G2) /\ E) by A58, XBOOLE_1:22
.= (dom (the_Source_of G2)) \/ ((the_Edges_of G2) /\ E) by FUNCT_2:def 1
.= (dom (the_Source_of G2)) \/ ((dom (the_Target_of G2)) /\ E) by FUNCT_2:def 1
.= (dom (the_Source_of G2)) \/ (dom ((the_Target_of G2) | E)) by RELAT_1:61
.= dom ((the_Source_of G2) +* ((the_Target_of G2) | E)) by FUNCT_4:def 1 ;

now :: thesis:

let x be object ; :: thesis:
assume x in dom (the_Source_of G3) ; :: thesis:
then x in the_Edges_of G3 ;
then x in union (the_Edges_of (rng B)) by GLIB_014:def 25;
then consider X being set such that
A60: ( x in X & X in the_Edges_of (rng B) ) by TARSKI:def 4;
consider G being _Graph such that
A61: ( G in rng B & X = the_Edges_of G ) by A60, GLIB_014:def 15;
consider z being object such that
A62: ( z in dom B & B . z = G ) by A61, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A62;
A63: z in dom h by A1;
A64: h . z in S2 by A1, FUNCT_1:3;
B . z in rng B by A62, FUNCT_1:3;
then A65: the_Source_of (B . z) in the_Source_of (rng B) by GLIB_014:def 16;
A66: B . z = the reverseEdgeDirections of h . z,A . z by A19;
A67: A . z is Subset of (the_Edges_of (h . z)) by A14;
A68: the_Source_of (h . z) in the_Source_of S2 by A64, GLIB_014:def 16;
A69: the_Target_of (h . z) in the_Target_of S2 by A64, GLIB_014:def 17;
A70: x in dom (the_Source_of (B . z)) by A60, A61, A62, FUNCT_2:def 1;
A71: the_Edges_of (B . z) = the_Edges_of (h . z) by A66, GLIB_007:4;
then A72: x in dom (the_Source_of (h . z)) by A60, A61, A62, FUNCT_2:def 1;
A73: x in dom (the_Target_of (h . z)) by A60, A61, A62, A71, FUNCT_2:def 1;

per cases ;

suppose A74: not x in A . z ; :: thesis:

then not x in (the_Edges_of (h . z)) /\ (A . z) by TARSKI:def 3, XBOOLE_1:17;
then not x in (dom (the_Target_of (h . z))) /\ (A . z) by FUNCT_2:def 1;
then A75: not x in dom ((the_Target_of (h . z)) | (A . z)) by RELAT_1:61;
not x in E

proof

assume x in E ; :: thesis:
then consider Y being set such that
A76: ( x in Y & Y in rng A ) by TARSKI:def 4;
consider z9 being object such that
A77: ( z9 in dom A & A . z9 = Y ) by A76, FUNCT_1:def 3;
reconsider z9 = z9 as Element of S1 by A77;
A78: x in A . z9 by A76, A77;
A . z9 is Subset of (the_Edges_of (h . z9)) by A14;
then A79: x in the_Edges_of (h . z9) by A78;
A80: z9 in dom h by A1;
A81: h . z9 in S2 by A1, FUNCT_1:3;
the_Edges_of (h . z) = the_Edges_of G by A62, A66, GLIB_007:4;
then x in the_Edges_of (h . z) by A60, A61;
then the_Edges_of (h . z) meets the_Edges_of (h . z9) by A79, XBOOLE_0:3;
then z = z9 by A63, A64, A80, A81, Def19, FUNCT_1:def 4;
hence contradiction by A74, A78; :: thesis:

end;

then not x in (the_Edges_of G2) /\ E by TARSKI:def 3, XBOOLE_1:17;
then not x in (dom (the_Target_of G2)) /\ E by FUNCT_2:def 1;
then A82: not x in dom ((the_Target_of G2) | E) by RELAT_1:61;
thus (the_Source_of G3) . x = (union (the_Source_of S3)) . x by GLIB_014:def 25
.= (the_Source_of (B . z)) . x by A65, A70, COMPUT_1:13
.= ((the_Source_of (h . z)) +* ((the_Target_of (h . z)) | (A . z))) . x by A66, A67, GLIB_007:def 1
.= (the_Source_of (h . z)) . x by A75, FUNCT_4:11
.= (union (the_Source_of S2)) . x by A68, A72, COMPUT_1:13
.= (the_Source_of G2) . x by GLIB_014:def 25
.= ((the_Source_of G2) +* ((the_Target_of G2) | E)) . x by A82, FUNCT_4:11 ; :: thesis:

end;

suppose A83: x in A . z ; :: thesis:

then x in (the_Edges_of (h . z)) /\ (A . z) by A67, XBOOLE_1:28;
then x in (dom (the_Target_of (h . z))) /\ (A . z) by FUNCT_2:def 1;
then A84: x in dom ((the_Target_of (h . z)) | (A . z)) by RELAT_1:61;
z in S1 ;
then z in dom A by PARTFUN1:def 2;
then A . z in rng A by FUNCT_1:3;
then A85: x in E by A83, TARSKI:def 4;
then x in (the_Edges_of G2) /\ E by XBOOLE_1:28;
then x in (dom (the_Target_of G2)) /\ E by FUNCT_2:def 1;
then A86: x in dom ((the_Target_of G2) | E) by RELAT_1:61;
thus (the_Source_of G3) . x = (union (the_Source_of S3)) . x by GLIB_014:def 25
.= (the_Source_of (B . z)) . x by A65, A70, COMPUT_1:13
.= ((the_Source_of (h . z)) +* ((the_Target_of (h . z)) | (A . z))) . x by A66, A67, GLIB_007:def 1
.= ((the_Target_of (h . z)) | (A . z)) . x by A84, FUNCT_4:13
.= (the_Target_of (h . z)) . x by A83, FUNCT_1:49
.= (union (the_Target_of S2)) . x by A69, A73, COMPUT_1:13
.= (the_Target_of G2) . x by GLIB_014:def 25
.= ((the_Target_of G2) | E) . x by A85, FUNCT_1:49
.= ((the_Source_of G2) +* ((the_Target_of G2) | E)) . x by A86, FUNCT_4:13 ; :: thesis:

end;

hence the_Source_of G3 = (the_Source_of G2) +* ((the_Target_of G2) | E) by A59, FUNCT_1:2; :: thesis:
A87: dom (the_Target_of G3) = the_Edges_of G3 by FUNCT_2:def 1
.= (the_Edges_of G2) \/ ((the_Edges_of G2) /\ E) by A58, XBOOLE_1:22
.= (dom (the_Target_of G2)) \/ ((the_Edges_of G2) /\ E) by FUNCT_2:def 1
.= (dom (the_Target_of G2)) \/ ((dom (the_Source_of G2)) /\ E) by FUNCT_2:def 1
.= (dom (the_Target_of G2)) \/ (dom ((the_Source_of G2) | E)) by RELAT_1:61
.= dom ((the_Target_of G2) +* ((the_Source_of G2) | E)) by FUNCT_4:def 1 ;

now :: thesis:

let x be object ; :: thesis:
assume x in dom (the_Target_of G3) ; :: thesis:
then x in the_Edges_of G3 ;
then x in union (the_Edges_of (rng B)) by GLIB_014:def 25;
then consider X being set such that
A88: ( x in X & X in the_Edges_of (rng B) ) by TARSKI:def 4;
consider G being _Graph such that
A89: ( G in rng B & X = the_Edges_of G ) by A88, GLIB_014:def 15;
consider z being object such that
A90: ( z in dom B & B . z = G ) by A89, FUNCT_1:def 3;
reconsider z = z as Element of S1 by A90;
A91: z in dom h by A1;
A92: h . z in S2 by A1, FUNCT_1:3;
B . z in rng B by A90, FUNCT_1:3;
then A93: the_Target_of (B . z) in the_Target_of (rng B) by GLIB_014:def 17;
A94: B . z = the reverseEdgeDirections of h . z,A . z by A19;
A95: A . z is Subset of (the_Edges_of (h . z)) by A14;
A96: the_Target_of (h . z) in the_Target_of S2 by A92, GLIB_014:def 17;
A97: the_Source_of (h . z) in the_Source_of S2 by A92, GLIB_014:def 16;
A98: x in dom (the_Target_of (B . z)) by A88, A89, A90, FUNCT_2:def 1;
A99: the_Edges_of (B . z) = the_Edges_of (h . z) by A94, GLIB_007:4;
then A100: x in dom (the_Target_of (h . z)) by A88, A89, A90, FUNCT_2:def 1;
A101: x in dom (the_Source_of (h . z)) by A88, A89, A90, A99, FUNCT_2:def 1;

per cases ;

suppose A102: not x in A . z ; :: thesis:

then not x in (the_Edges_of (h . z)) /\ (A . z) by TARSKI:def 3, XBOOLE_1:17;
then not x in (dom (the_Source_of (h . z))) /\ (A . z) by FUNCT_2:def 1;
then A103: not x in dom ((the_Source_of (h . z)) | (A . z)) by RELAT_1:61;
not x in E

proof

assume x in E ; :: thesis:
then consider Y being set such that
A104: ( x in Y & Y in rng A ) by TARSKI:def 4;
consider z9 being object such that
A105: ( z9 in dom A & A . z9 = Y ) by A104, FUNCT_1:def 3;
reconsider z9 = z9 as Element of S1 by A105;
A106: x in A . z9 by A104, A105;
A . z9 is Subset of (the_Edges_of (h . z9)) by A14;
then A107: x in the_Edges_of (h . z9) by A106;
A108: z9 in dom h by A1;
A109: h . z9 in S2 by A1, FUNCT_1:3;
the_Edges_of (h . z) = the_Edges_of G by A90, A94, GLIB_007:4;
then x in the_Edges_of (h . z) by A88, A89;
then the_Edges_of (h . z) meets the_Edges_of (h . z9) by A107, XBOOLE_0:3;
then z = z9 by A91, A92, A108, A109, Def19, FUNCT_1:def 4;
hence contradiction by A102, A106; :: thesis:

end;

then not x in (the_Edges_of G2) /\ E by TARSKI:def 3, XBOOLE_1:17;
then not x in (dom (the_Source_of G2)) /\ E by FUNCT_2:def 1;
then A110: not x in dom ((the_Source_of G2) | E) by RELAT_1:61;
thus (the_Target_of G3) . x = (union (the_Target_of S3)) . x by GLIB_014:def 25
.= (the_Target_of (B . z)) . x by A93, A98, COMPUT_1:13
.= ((the_Target_of (h . z)) +* ((the_Source_of (h . z)) | (A . z))) . x by A94, A95, GLIB_007:def 1
.= (the_Target_of (h . z)) . x by A103, FUNCT_4:11
.= (union (the_Target_of S2)) . x by A96, A100, COMPUT_1:13
.= (the_Target_of G2) . x by GLIB_014:def 25
.= ((the_Target_of G2) +* ((the_Source_of G2) | E)) . x by A110, FUNCT_4:11 ; :: thesis:

end;

suppose A111: x in A . z ; :: thesis:

then x in (the_Edges_of (h . z)) /\ (A . z) by A95, XBOOLE_1:28;
then x in (dom (the_Source_of (h . z))) /\ (A . z) by FUNCT_2:def 1;
then A112: x in dom ((the_Source_of (h . z)) | (A . z)) by RELAT_1:61;
z in S1 ;
then z in dom A by PARTFUN1:def 2;
then A . z in rng A by FUNCT_1:3;
then A113: x in E by A111, TARSKI:def 4;
then x in (the_Edges_of G2) /\ E by XBOOLE_1:28;
then x in (dom (the_Source_of G2)) /\ E by FUNCT_2:def 1;
then A114: x in dom ((the_Source_of G2) | E) by RELAT_1:61;
thus (the_Target_of G3) . x = (union (the_Target_of S3)) . x by GLIB_014:def 25
.= (the_Target_of (B . z)) . x by A93, A98, COMPUT_1:13
.= ((the_Target_of (h . z)) +* ((the_Source_of (h . z)) | (A . z))) . x by A94, A95, GLIB_007:def 1
.= ((the_Source_of (h . z)) | (A . z)) . x by A112, FUNCT_4:13
.= (the_Source_of (h . z)) . x by A111, FUNCT_1:49
.= (union (the_Source_of S2)) . x by A97, A101, COMPUT_1:13
.= (the_Source_of G2) . x by GLIB_014:def 25
.= ((the_Source_of G2) | E) . x by A113, FUNCT_1:49
.= ((the_Target_of G2) +* ((the_Source_of G2) | E)) . x by A114, FUNCT_4:13 ; :: thesis:

end;

hence the_Target_of G3 = (the_Target_of G2) +* ((the_Source_of G2) | E) by A87, FUNCT_1:2; :: thesis:

end;

hence G3 is reverseEdgeDirections of G2,E by GLIB_007:def 1; :: thesis: