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₁[ 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₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( x in the_Edges_of G2 & S₁[x,y1] & S₁[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₁[x,y1] or not S₁[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₁[x,y1] ; :: thesis: ( not S₁[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₁[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;

A15: for x being object st x in the_Edges_of G2 holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in the_Edges_of G2 implies ex y being object st S₁[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₁[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₁[x,e]
thus S₁[x,e] by A16, A17, GLIB_009:def 3; :: thesis: verum

end;

consider h being Function such that
A18: dom h = the_Edges_of G2 and
A19: for x being object st x in the_Edges_of G2 holds
S₁[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 ;

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) ) )

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) ) )

hereby :: thesis: ( y in E2 implies 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;

assume A23: y in E2 ; :: thesis: 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;

then A40: rng ((h * (G _E)) | E1) = E2 by TARSKI:2;
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 ) )

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 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;

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 )
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

per cases ( ( f . v = u1 & f . w = u2 ) or ( f . v = u2 & f . w = u1 ) ) by A45, A47, GLIB_000:15;

suppose ( f . v = u1 & f . w = u2 ) ; :: thesis: h . ((G _E) . e) Joins f . v,f . w,G2

hence h . ((G _E) . e) Joins f . v,f . w,G2 by A47; :: thesis: verum

end;

suppose ( f . v = u2 & f . w = u1 ) ; :: thesis: h . ((G _E) . e) Joins f . v,f . w,G2

hence h . ((G _E) . e) Joins f . v,f . w,G2 by A47, GLIB_000:14; :: thesis: verum

end;

end;

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

end;

then reconsider F = [f,g] as PGraphMapping of G3,G4 by Th8;
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

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

proof

per cases ( ( v1 = w1 & v2 = w2 ) or ( v1 = w2 & v2 = w1 ) ) by A55, A60, GLIB_000:15;

suppose ( v1 = w1 & v2 = w2 ) ; :: thesis: (G _E) . x2 Joins v1,v2,G2

hence (G _E) . x2 Joins v1,v2,G2 by A60; :: thesis: verum

end;

suppose ( v1 = w2 & v2 = w1 ) ; :: thesis: (G _E) . x2 Joins v1,v2,G2

hence (G _E) . x2 Joins v1,v2,G2 by A60, GLIB_000:14; :: thesis: verum

end;

end;

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

end;

then F is one-to-one by A1, FUNCT_1:def 4;
hence G4 is G3 -isomorphic by A49, A50; :: thesis: verum