let G1 be _Graph; :: thesis: for G2 being G1 -isomorphic _Graph

for G3 being removeParallelEdges of G1

for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

let G2 be G1 -isomorphic _Graph; :: thesis: for G3 being removeParallelEdges of G1

for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

let G3 be removeParallelEdges of G1; :: thesis: for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

let G4 be removeParallelEdges of G2; :: thesis: G4 is G3 -isomorphic

consider G being PGraphMapping of G1,G2 such that

A1: G is isomorphism by Def23;

consider E1 being RepEdgeSelection of G1 such that

A2: G3 is inducedSubgraph of G1, the_Vertices_of G1,E1 by GLIB_009:def 7;

consider E2 being RepEdgeSelection of G2 such that

A3: G4 is inducedSubgraph of G2, the_Vertices_of G2,E2 by GLIB_009:def 7;

A4: ( G1 .edgesBetween (the_Vertices_of G1) = the_Edges_of G1 & G2 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2 ) by GLIB_000:34;

( the_Vertices_of G1 c= the_Vertices_of G1 & the_Vertices_of G2 c= the_Vertices_of G2 ) ;

then A5: ( the_Edges_of G3 = E1 & the_Edges_of G4 = E2 ) by A2, A3, A4, GLIB_000:def 37;

A6: ( the_Vertices_of G3 = the_Vertices_of G1 & the_Vertices_of G4 = the_Vertices_of G2 ) by GLIB_000:def 33;

then reconsider f = G _V as PartFunc of (the_Vertices_of G3),(the_Vertices_of G4) ;

defpred S_{1}[ object , object ] means ( $2 in E2 & [$1,$2] in EdgeAdjEqRel G2 );

A7: for x, y1, y2 being object st x in the_Edges_of G2 & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2

ex y being object st S_{1}[x,y]

A18: dom h = the_Edges_of G2 and

A19: for x being object st x in the_Edges_of G2 holds

S_{1}[x,h . x]
from FUNCT_1:sch 2(A7, A15);

set g = (h * (G _E)) | E1;

dom h = rng (G _E) by A1, A18, Def12;

then A20: ( dom (h * (G _E)) = dom (G _E) & rng (h * (G _E)) = rng h ) by RELAT_1:27, RELAT_1:28;

then A21: dom ((h * (G _E)) | E1) = (dom (G _E)) /\ E1 by RELAT_1:61

.= (the_Edges_of G1) /\ E1 by A1, Def11

.= E1 by XBOOLE_1:28 ;

then reconsider g = (h * (G _E)) | E1 as PartFunc of (the_Edges_of G3),(the_Edges_of G4) by A5, A21, RELSET_1:4;

dom f = the_Vertices_of G3 by A1, A6, Def11;

then A49: F is total by A5, A21;

rng f = the_Vertices_of G4 by A1, A6, Def12;

then A50: F is onto by A5, A40;

hence G4 is G3 -isomorphic by A49, A50; :: thesis: verum

for G3 being removeParallelEdges of G1

for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

let G2 be G1 -isomorphic _Graph; :: thesis: for G3 being removeParallelEdges of G1

for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

let G3 be removeParallelEdges of G1; :: thesis: for G4 being removeParallelEdges of G2 holds G4 is G3 -isomorphic

let G4 be removeParallelEdges of G2; :: thesis: G4 is G3 -isomorphic

consider G being PGraphMapping of G1,G2 such that

A1: G is isomorphism by Def23;

consider E1 being RepEdgeSelection of G1 such that

A2: G3 is inducedSubgraph of G1, the_Vertices_of G1,E1 by GLIB_009:def 7;

consider E2 being RepEdgeSelection of G2 such that

A3: G4 is inducedSubgraph of G2, the_Vertices_of G2,E2 by GLIB_009:def 7;

A4: ( G1 .edgesBetween (the_Vertices_of G1) = the_Edges_of G1 & G2 .edgesBetween (the_Vertices_of G2) = the_Edges_of G2 ) by GLIB_000:34;

( the_Vertices_of G1 c= the_Vertices_of G1 & the_Vertices_of G2 c= the_Vertices_of G2 ) ;

then A5: ( the_Edges_of G3 = E1 & the_Edges_of G4 = E2 ) by A2, A3, A4, GLIB_000:def 37;

A6: ( the_Vertices_of G3 = the_Vertices_of G1 & the_Vertices_of G4 = the_Vertices_of G2 ) by GLIB_000:def 33;

then reconsider f = G _V as PartFunc of (the_Vertices_of G3),(the_Vertices_of G4) ;

defpred S

A7: for x, y1, y2 being object st x in the_Edges_of G2 & S

y1 = y2

proof

A15:
for x being object st x in the_Edges_of G2 holds
let x, y1, y2 be object ; :: thesis: ( x in the_Edges_of G2 & S_{1}[x,y1] & S_{1}[x,y2] implies y1 = y2 )

set v1 = (the_Source_of G2) . x;

set v2 = (the_Target_of G2) . x;

assume x in the_Edges_of G2 ; :: thesis: ( not S_{1}[x,y1] or not S_{1}[x,y2] or y1 = y2 )

then A8: x Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 by GLIB_000:def 13;

then consider e being object such that

( e Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e in E2 ) and

A9: for e9 being object st e9 Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e9 in E2 holds

e9 = e by GLIB_009:def 5;

assume A10: S_{1}[x,y1]
; :: thesis: ( not S_{1}[x,y2] or y1 = y2 )

then consider w1, w2 being object such that

A11: ( x Joins w1,w2,G2 & y1 Joins w1,w2,G2 ) by GLIB_009:def 3;

( ( w1 = (the_Source_of G2) . x & w2 = (the_Target_of G2) . x ) or ( w1 = (the_Target_of G2) . x & w2 = (the_Source_of G2) . x ) ) by A8, A11, GLIB_000:15;

then A12: y1 = e by A9, A10, A11, GLIB_000:14;

assume A13: S_{1}[x,y2]
; :: thesis: y1 = y2

then consider u1, u2 being object such that

A14: ( x Joins u1,u2,G2 & y2 Joins u1,u2,G2 ) by GLIB_009:def 3;

( ( u1 = (the_Source_of G2) . x & u2 = (the_Target_of G2) . x ) or ( u1 = (the_Target_of G2) . x & u2 = (the_Source_of G2) . x ) ) by A8, A14, GLIB_000:15;

then y2 Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 by A14, GLIB_000:14;

hence y1 = y2 by A9, A12, A13; :: thesis: verum

end;set v1 = (the_Source_of G2) . x;

set v2 = (the_Target_of G2) . x;

assume x in the_Edges_of G2 ; :: thesis: ( not S

then A8: x Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 by GLIB_000:def 13;

then consider e being object such that

( e Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e in E2 ) and

A9: for e9 being object st e9 Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e9 in E2 holds

e9 = e by GLIB_009:def 5;

assume A10: S

then consider w1, w2 being object such that

A11: ( x Joins w1,w2,G2 & y1 Joins w1,w2,G2 ) by GLIB_009:def 3;

( ( w1 = (the_Source_of G2) . x & w2 = (the_Target_of G2) . x ) or ( w1 = (the_Target_of G2) . x & w2 = (the_Source_of G2) . x ) ) by A8, A11, GLIB_000:15;

then A12: y1 = e by A9, A10, A11, GLIB_000:14;

assume A13: S

then consider u1, u2 being object such that

A14: ( x Joins u1,u2,G2 & y2 Joins u1,u2,G2 ) by GLIB_009:def 3;

( ( u1 = (the_Source_of G2) . x & u2 = (the_Target_of G2) . x ) or ( u1 = (the_Target_of G2) . x & u2 = (the_Source_of G2) . x ) ) by A8, A14, GLIB_000:15;

then y2 Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 by A14, GLIB_000:14;

hence y1 = y2 by A9, A12, A13; :: thesis: verum

ex y being object st S

proof

consider h being Function such that
let x be object ; :: thesis: ( x in the_Edges_of G2 implies ex y being object st S_{1}[x,y] )

set v1 = (the_Source_of G2) . x;

set v2 = (the_Target_of G2) . x;

assume x in the_Edges_of G2 ; :: thesis: ex y being object st S_{1}[x,y]

then A16: x Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 by GLIB_000:def 13;

then consider e being object such that

A17: ( e Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e in E2 ) and

for e9 being object st e9 Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e9 in E2 holds

e9 = e by GLIB_009:def 5;

take e ; :: thesis: S_{1}[x,e]

thus S_{1}[x,e]
by A16, A17, GLIB_009:def 3; :: thesis: verum

end;set v1 = (the_Source_of G2) . x;

set v2 = (the_Target_of G2) . x;

assume x in the_Edges_of G2 ; :: thesis: ex y being object st S

then A16: x Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 by GLIB_000:def 13;

then consider e being object such that

A17: ( e Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e in E2 ) and

for e9 being object st e9 Joins (the_Source_of G2) . x,(the_Target_of G2) . x,G2 & e9 in E2 holds

e9 = e by GLIB_009:def 5;

take e ; :: thesis: S

thus S

A18: dom h = the_Edges_of G2 and

A19: for x being object st x in the_Edges_of G2 holds

S

set g = (h * (G _E)) | E1;

dom h = rng (G _E) by A1, A18, Def12;

then A20: ( dom (h * (G _E)) = dom (G _E) & rng (h * (G _E)) = rng h ) by RELAT_1:27, RELAT_1:28;

then A21: dom ((h * (G _E)) | E1) = (dom (G _E)) /\ E1 by RELAT_1:61

.= (the_Edges_of G1) /\ E1 by A1, Def11

.= E1 by XBOOLE_1:28 ;

now :: thesis: for y being object holds

( ( y in rng ((h * (G _E)) | E1) implies y in E2 ) & ( y in E2 implies y in rng ((h * (G _E)) | E1) ) )

then A40:
rng ((h * (G _E)) | E1) = E2
by TARSKI:2;( ( y in rng ((h * (G _E)) | E1) implies y in E2 ) & ( y in E2 implies y in rng ((h * (G _E)) | E1) ) )

let y be object ; :: thesis: ( ( y in rng ((h * (G _E)) | E1) implies y in E2 ) & ( y in E2 implies y in rng ((h * (G _E)) | E1) ) )

then A24: y in the_Edges_of G2 ;

set v1 = (the_Source_of G2) . y;

set v2 = (the_Target_of G2) . y;

A25: y Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 by A24, GLIB_000:def 13;

then consider e being object such that

( e Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 & e in E2 ) and

A26: for e9 being object st e9 Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 & e9 in E2 holds

e9 = e by GLIB_009:def 5;

y in rng (G _E) by A1, A24, Def12;

then consider x0 being object such that

A27: ( x0 in dom (G _E) & (G _E) . x0 = y ) by FUNCT_1:def 3;

set u1 = (the_Source_of G1) . x0;

set u2 = (the_Target_of G1) . x0;

A28: ( (the_Source_of G1) . x0 in dom (G _V) & (the_Target_of G1) . x0 in dom (G _V) ) by A27, Th5;

A29: x0 Joins (the_Source_of G1) . x0,(the_Target_of G1) . x0,G1 by A27, GLIB_000:def 13;

then consider x being object such that

A30: ( x Joins (the_Source_of G1) . x0,(the_Target_of G1) . x0,G1 & x in E1 ) and

for e9 being object st e9 Joins (the_Source_of G1) . x0,(the_Target_of G1) . x0,G1 & e9 in E1 holds

e9 = x by GLIB_009:def 5;

x in the_Edges_of G1 by A30;

then A31: x in dom (G _E) by A1, Def11;

then A32: (G _E) . x Joins (G _V) . ((the_Source_of G1) . x0),(G _V) . ((the_Target_of G1) . x0),G2 by A28, A30, Th4;

(G _E) . x0 Joins (G _V) . ((the_Source_of G1) . x0),(G _V) . ((the_Target_of G1) . x0),G2 by A27, A28, A29, Th4;

then ( ( (G _V) . ((the_Source_of G1) . x0) = (the_Source_of G2) . y & (G _V) . ((the_Target_of G1) . x0) = (the_Target_of G2) . y ) or ( (G _V) . ((the_Source_of G1) . x0) = (the_Target_of G2) . y & (G _V) . ((the_Target_of G1) . x0) = (the_Source_of G2) . y ) ) by A25, A27, GLIB_000:15;

then A33: (G _E) . x Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 by A32, GLIB_000:14;

A34: (G _E) . x in the_Edges_of G2 by A33, GLIB_000:def 13;

then A35: ( h . ((G _E) . x) in E2 & [((G _E) . x),(h . ((G _E) . x))] in EdgeAdjEqRel G2 ) by A19;

then consider w1, w2 being object such that

A36: ( (G _E) . x Joins w1,w2,G2 & h . ((G _E) . x) Joins w1,w2,G2 ) by GLIB_009:def 3;

( ( (the_Source_of G2) . y = w1 & (the_Target_of G2) . y = w2 ) or ( (the_Source_of G2) . y = w2 & (the_Target_of G2) . y = w1 ) ) by A33, A36, GLIB_000:15;

then A37: ( y = e & h . ((G _E) . x) = e ) by A23, A25, A26, A35, A36, GLIB_000:14;

A38: x in dom (h * (G _E)) by A18, A31, A34, FUNCT_1:11;

then A39: x in dom ((h * (G _E)) | E1) by A30, RELAT_1:57;

y = (h * (G _E)) . x by A37, A38, FUNCT_1:12

.= ((h * (G _E)) | E1) . x by A30, FUNCT_1:49 ;

hence y in rng ((h * (G _E)) | E1) by A39, FUNCT_1:def 3; :: thesis: verum

end;hereby :: thesis: ( y in E2 implies y in rng ((h * (G _E)) | E1) )

assume A23:
y in E2
; :: thesis: y in rng ((h * (G _E)) | E1)assume
y in rng ((h * (G _E)) | E1)
; :: thesis: y in E2

then y in rng h by A20, RELAT_1:70, TARSKI:def 3;

then consider x being object such that

A22: ( x in dom h & y = h . x ) by FUNCT_1:def 3;

thus y in E2 by A18, A19, A22; :: thesis: verum

end;then y in rng h by A20, RELAT_1:70, TARSKI:def 3;

then consider x being object such that

A22: ( x in dom h & y = h . x ) by FUNCT_1:def 3;

thus y in E2 by A18, A19, A22; :: thesis: verum

then A24: y in the_Edges_of G2 ;

set v1 = (the_Source_of G2) . y;

set v2 = (the_Target_of G2) . y;

A25: y Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 by A24, GLIB_000:def 13;

then consider e being object such that

( e Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 & e in E2 ) and

A26: for e9 being object st e9 Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 & e9 in E2 holds

e9 = e by GLIB_009:def 5;

y in rng (G _E) by A1, A24, Def12;

then consider x0 being object such that

A27: ( x0 in dom (G _E) & (G _E) . x0 = y ) by FUNCT_1:def 3;

set u1 = (the_Source_of G1) . x0;

set u2 = (the_Target_of G1) . x0;

A28: ( (the_Source_of G1) . x0 in dom (G _V) & (the_Target_of G1) . x0 in dom (G _V) ) by A27, Th5;

A29: x0 Joins (the_Source_of G1) . x0,(the_Target_of G1) . x0,G1 by A27, GLIB_000:def 13;

then consider x being object such that

A30: ( x Joins (the_Source_of G1) . x0,(the_Target_of G1) . x0,G1 & x in E1 ) and

for e9 being object st e9 Joins (the_Source_of G1) . x0,(the_Target_of G1) . x0,G1 & e9 in E1 holds

e9 = x by GLIB_009:def 5;

x in the_Edges_of G1 by A30;

then A31: x in dom (G _E) by A1, Def11;

then A32: (G _E) . x Joins (G _V) . ((the_Source_of G1) . x0),(G _V) . ((the_Target_of G1) . x0),G2 by A28, A30, Th4;

(G _E) . x0 Joins (G _V) . ((the_Source_of G1) . x0),(G _V) . ((the_Target_of G1) . x0),G2 by A27, A28, A29, Th4;

then ( ( (G _V) . ((the_Source_of G1) . x0) = (the_Source_of G2) . y & (G _V) . ((the_Target_of G1) . x0) = (the_Target_of G2) . y ) or ( (G _V) . ((the_Source_of G1) . x0) = (the_Target_of G2) . y & (G _V) . ((the_Target_of G1) . x0) = (the_Source_of G2) . y ) ) by A25, A27, GLIB_000:15;

then A33: (G _E) . x Joins (the_Source_of G2) . y,(the_Target_of G2) . y,G2 by A32, GLIB_000:14;

A34: (G _E) . x in the_Edges_of G2 by A33, GLIB_000:def 13;

then A35: ( h . ((G _E) . x) in E2 & [((G _E) . x),(h . ((G _E) . x))] in EdgeAdjEqRel G2 ) by A19;

then consider w1, w2 being object such that

A36: ( (G _E) . x Joins w1,w2,G2 & h . ((G _E) . x) Joins w1,w2,G2 ) by GLIB_009:def 3;

( ( (the_Source_of G2) . y = w1 & (the_Target_of G2) . y = w2 ) or ( (the_Source_of G2) . y = w2 & (the_Target_of G2) . y = w1 ) ) by A33, A36, GLIB_000:15;

then A37: ( y = e & h . ((G _E) . x) = e ) by A23, A25, A26, A35, A36, GLIB_000:14;

A38: x in dom (h * (G _E)) by A18, A31, A34, FUNCT_1:11;

then A39: x in dom ((h * (G _E)) | E1) by A30, RELAT_1:57;

y = (h * (G _E)) . x by A37, A38, FUNCT_1:12

.= ((h * (G _E)) | E1) . x by A30, FUNCT_1:49 ;

hence y in rng ((h * (G _E)) | E1) by A39, FUNCT_1:def 3; :: thesis: verum

then reconsider g = (h * (G _E)) | E1 as PartFunc of (the_Edges_of G3),(the_Edges_of G4) by A5, A21, RELSET_1:4;

now :: thesis: ( ( for e being object st e in dom g holds

( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G3 holds

g . e Joins f . v,f . w,G4 ) )

assume A41: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G3 implies g . e Joins f . v,f . w,G4 )

then A42: ( e in E1 & e in dom (h * (G _E)) ) by RELAT_1:57;

then A43: ( e in dom (G _E) & (G _E) . e in dom h ) by FUNCT_1:11;

assume A44: e Joins v,w,G3 ; :: thesis: g . e Joins f . v,f . w,G4

( v is set & w is set ) by TARSKI:1;

then e Joins v,w,G1 by A44, GLIB_000:72;

then A45: (G _E) . e Joins f . v,f . w,G2 by A41, A43, Th4;

A46: ( h . ((G _E) . e) in E2 & [((G _E) . e),(h . ((G _E) . e))] in EdgeAdjEqRel G2 ) by A18, A19, A43;

then consider u1, u2 being object such that

A47: ( (G _E) . e Joins u1,u2,G2 & h . ((G _E) . e) Joins u1,u2,G2 ) by GLIB_009:def 3;

h . ((G _E) . e) Joins f . v,f . w,G2

g . e = (h * (G _E)) . e by A42, FUNCT_1:49

.= h . ((G _E) . e) by A42, FUNCT_1:12 ;

hence g . e Joins f . v,f . w,G4 by A48; :: thesis: verum

end;

then reconsider F = [f,g] as PGraphMapping of G3,G4 by Th8;( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) ) & ( for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G3 holds

g . e Joins f . v,f . w,G4 ) )

hereby :: thesis: for e, v, w being object st e in dom g & v in dom f & w in dom f & e Joins v,w,G3 holds

g . e Joins f . v,f . w,G4

let e, v, w be object ; :: thesis: ( e in dom g & v in dom f & w in dom f & e Joins v,w,G3 implies g . e Joins f . v,f . w,G4 )g . e Joins f . v,f . w,G4

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) )

set v = (the_Source_of G3) . e;

set w = (the_Target_of G3) . e;

assume e in dom g ; :: thesis: ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f )

then e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by GLIB_000:def 13;

then ( (the_Source_of G3) . e in the_Vertices_of G3 & (the_Target_of G3) . e in the_Vertices_of G3 ) by GLIB_000:13;

then ( (the_Source_of G3) . e in the_Vertices_of G1 & (the_Target_of G3) . e in the_Vertices_of G1 ) ;

hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A1, Def11; :: thesis: verum

end;set v = (the_Source_of G3) . e;

set w = (the_Target_of G3) . e;

assume e in dom g ; :: thesis: ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f )

then e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by GLIB_000:def 13;

then ( (the_Source_of G3) . e in the_Vertices_of G3 & (the_Target_of G3) . e in the_Vertices_of G3 ) by GLIB_000:13;

then ( (the_Source_of G3) . e in the_Vertices_of G1 & (the_Target_of G3) . e in the_Vertices_of G1 ) ;

hence ( (the_Source_of G3) . e in dom f & (the_Target_of G3) . e in dom f ) by A1, Def11; :: thesis: verum

assume A41: ( e in dom g & v in dom f & w in dom f ) ; :: thesis: ( e Joins v,w,G3 implies g . e Joins f . v,f . w,G4 )

then A42: ( e in E1 & e in dom (h * (G _E)) ) by RELAT_1:57;

then A43: ( e in dom (G _E) & (G _E) . e in dom h ) by FUNCT_1:11;

assume A44: e Joins v,w,G3 ; :: thesis: g . e Joins f . v,f . w,G4

( v is set & w is set ) by TARSKI:1;

then e Joins v,w,G1 by A44, GLIB_000:72;

then A45: (G _E) . e Joins f . v,f . w,G2 by A41, A43, Th4;

A46: ( h . ((G _E) . e) in E2 & [((G _E) . e),(h . ((G _E) . e))] in EdgeAdjEqRel G2 ) by A18, A19, A43;

then consider u1, u2 being object such that

A47: ( (G _E) . e Joins u1,u2,G2 & h . ((G _E) . e) Joins u1,u2,G2 ) by GLIB_009:def 3;

h . ((G _E) . e) Joins f . v,f . w,G2

proof
end;

then A48:
h . ((G _E) . e) Joins f . v,f . w,G4
by A5, A46, GLIB_000:73;g . e = (h * (G _E)) . e by A42, FUNCT_1:49

.= h . ((G _E) . e) by A42, FUNCT_1:12 ;

hence g . e Joins f . v,f . w,G4 by A48; :: thesis: verum

dom f = the_Vertices_of G3 by A1, A6, Def11;

then A49: F is total by A5, A21;

rng f = the_Vertices_of G4 by A1, A6, Def12;

then A50: F is onto by A5, A40;

now :: thesis: for x1, x2 being object st x1 in dom g & x2 in dom g & g . x1 = g . x2 holds

x1 = x2

then
F is one-to-one
by A1, FUNCT_1:def 4;x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 implies x1 = x2 )

assume A51: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis: x1 = x2

then A52: ( x1 in E1 & x1 in dom (h * (G _E)) & x2 in E1 & x2 in dom (h * (G _E)) ) by RELAT_1:57;

then A53: ( x1 in dom (G _E) & (G _E) . x1 in dom h & x2 in dom (G _E) & (G _E) . x2 in dom h ) by FUNCT_1:11;

then A54: ( h . ((G _E) . x1) in E2 & [((G _E) . x1),(h . ((G _E) . x1))] in EdgeAdjEqRel G2 & [((G _E) . x2),(h . ((G _E) . x2))] in EdgeAdjEqRel G2 ) by A18, A19;

then consider v1, v2 being object such that

A55: ( (G _E) . x1 Joins v1,v2,G2 & h . ((G _E) . x1) Joins v1,v2,G2 ) by GLIB_009:def 3;

(G _E) . x1 in rng (G _E) by A53, FUNCT_1:3;

then ( (the_Source_of G2) . ((G _E) . x1) in rng (G _V) & (the_Target_of G2) . ((G _E) . x1) in rng (G _V) ) by Th6;

then A56: ( v1 in rng (G _V) & v2 in rng (G _V) ) by A55, GLIB_000:def 13;

then consider u1 being object such that

A57: ( u1 in dom (G _V) & (G _V) . u1 = v1 ) by FUNCT_1:def 3;

consider u2 being object such that

A58: ( u2 in dom (G _V) & (G _V) . u2 = v2 ) by A56, FUNCT_1:def 3;

A59: x1 Joins u1,u2,G1 by A1, A53, A55, A57, A58, Def15;

h . ((G _E) . x1) = (h * (G _E)) . x1 by A52, FUNCT_1:12

.= g . x2 by A51, A52, FUNCT_1:49

.= (h * (G _E)) . x2 by A52, FUNCT_1:49

.= h . ((G _E) . x2) by A52, FUNCT_1:12 ;

then consider w1, w2 being object such that

A60: ( (G _E) . x2 Joins w1,w2,G2 & h . ((G _E) . x1) Joins w1,w2,G2 ) by A54, GLIB_009:def 3;

(G _E) . x2 Joins v1,v2,G2

then consider e being object such that

( e Joins u1,u2,G1 & e in E1 ) and

A62: for e9 being object st e9 Joins u1,u2,G1 & e9 in E1 holds

e9 = e by GLIB_009:def 5;

( x1 = e & x2 = e ) by A52, A59, A61, A62;

hence x1 = x2 ; :: thesis: verum

end;assume A51: ( x1 in dom g & x2 in dom g & g . x1 = g . x2 ) ; :: thesis: x1 = x2

then A52: ( x1 in E1 & x1 in dom (h * (G _E)) & x2 in E1 & x2 in dom (h * (G _E)) ) by RELAT_1:57;

then A53: ( x1 in dom (G _E) & (G _E) . x1 in dom h & x2 in dom (G _E) & (G _E) . x2 in dom h ) by FUNCT_1:11;

then A54: ( h . ((G _E) . x1) in E2 & [((G _E) . x1),(h . ((G _E) . x1))] in EdgeAdjEqRel G2 & [((G _E) . x2),(h . ((G _E) . x2))] in EdgeAdjEqRel G2 ) by A18, A19;

then consider v1, v2 being object such that

A55: ( (G _E) . x1 Joins v1,v2,G2 & h . ((G _E) . x1) Joins v1,v2,G2 ) by GLIB_009:def 3;

(G _E) . x1 in rng (G _E) by A53, FUNCT_1:3;

then ( (the_Source_of G2) . ((G _E) . x1) in rng (G _V) & (the_Target_of G2) . ((G _E) . x1) in rng (G _V) ) by Th6;

then A56: ( v1 in rng (G _V) & v2 in rng (G _V) ) by A55, GLIB_000:def 13;

then consider u1 being object such that

A57: ( u1 in dom (G _V) & (G _V) . u1 = v1 ) by FUNCT_1:def 3;

consider u2 being object such that

A58: ( u2 in dom (G _V) & (G _V) . u2 = v2 ) by A56, FUNCT_1:def 3;

A59: x1 Joins u1,u2,G1 by A1, A53, A55, A57, A58, Def15;

h . ((G _E) . x1) = (h * (G _E)) . x1 by A52, FUNCT_1:12

.= g . x2 by A51, A52, FUNCT_1:49

.= (h * (G _E)) . x2 by A52, FUNCT_1:49

.= h . ((G _E) . x2) by A52, FUNCT_1:12 ;

then consider w1, w2 being object such that

A60: ( (G _E) . x2 Joins w1,w2,G2 & h . ((G _E) . x1) Joins w1,w2,G2 ) by A54, GLIB_009:def 3;

(G _E) . x2 Joins v1,v2,G2

proof
end;

then A61:
x2 Joins u1,u2,G1
by A1, A53, A57, A58, Def15;then consider e being object such that

( e Joins u1,u2,G1 & e in E1 ) and

A62: for e9 being object st e9 Joins u1,u2,G1 & e9 in E1 holds

e9 = e by GLIB_009:def 5;

( x1 = e & x2 = e ) by A52, A59, A61, A62;

hence x1 = x2 ; :: thesis: verum

hence G4 is G3 -isomorphic by A49, A50; :: thesis: verum