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_Edges_of G1 & G2 .edgesBetween () = 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 ;
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 (),() ;
defpred S1[ 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 & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( x in the_Edges_of G2 & S1[x,y1] & S1[x,y2] implies y1 = y2 )
set v1 = () . x;
set v2 = () . x;
assume x in the_Edges_of G2 ; :: thesis: ( not S1[x,y1] or not S1[x,y2] or y1 = y2 )
then A8: x Joins () . x,() . x,G2 by GLIB_000:def 13;
then consider e being object such that
( e Joins () . x,() . x,G2 & e in E2 ) and
A9: for e9 being object st e9 Joins () . x,() . x,G2 & e9 in E2 holds
e9 = e by GLIB_009:def 5;
assume A10: S1[x,y1] ; :: thesis: ( not S1[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 = () . x & w2 = () . x ) or ( w1 = () . x & w2 = () . x ) ) by ;
then A12: y1 = e by ;
assume A13: S1[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 = () . x & u2 = () . x ) or ( u1 = () . x & u2 = () . x ) ) by ;
then y2 Joins () . x,() . x,G2 by ;
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 S1[x,y]
proof
let x be object ; :: thesis: ( x in the_Edges_of G2 implies ex y being object st S1[x,y] )
set v1 = () . x;
set v2 = () . x;
assume x in the_Edges_of G2 ; :: thesis: ex y being object st S1[x,y]
then A16: x Joins () . x,() . x,G2 by GLIB_000:def 13;
then consider e being object such that
A17: ( e Joins () . x,() . x,G2 & e in E2 ) and
for e9 being object st e9 Joins () . x,() . x,G2 & e9 in E2 holds
e9 = e by GLIB_009:def 5;
take e ; :: thesis: S1[x,e]
thus S1[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
S1[x,h . x] from set g = (h * (G _E)) | E1;
dom h = rng (G _E) by ;
then A20: ( dom (h * (G _E)) = dom (G _E) & rng (h * (G _E)) = rng h ) by ;
then A21: dom ((h * (G _E)) | E1) = (dom (G _E)) /\ E1 by RELAT_1:61
.= () /\ E1 by
.= 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 ;
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 ; :: 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 = () . y;
set v2 = () . y;
A25: y Joins () . y,() . y,G2 by ;
then consider e being object such that
( e Joins () . y,() . y,G2 & e in E2 ) and
A26: for e9 being object st e9 Joins () . y,() . y,G2 & e9 in E2 holds
e9 = e by GLIB_009:def 5;
y in rng (G _E) by ;
then consider x0 being object such that
A27: ( x0 in dom (G _E) & (G _E) . x0 = y ) by FUNCT_1:def 3;
set u1 = () . x0;
set u2 = () . x0;
A28: ( (the_Source_of G1) . x0 in dom (G _V) & () . x0 in dom (G _V) ) by ;
A29: x0 Joins () . x0,() . x0,G1 by ;
then consider x being object such that
A30: ( x Joins () . x0,() . x0,G1 & x in E1 ) and
for e9 being object st e9 Joins () . x0,() . 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 ;
then A32: (G _E) . x Joins (G _V) . (() . x0),(G _V) . (() . x0),G2 by ;
(G _E) . x0 Joins (G _V) . (() . x0),(G _V) . (() . x0),G2 by A27, A28, A29, Th4;
then ( ( (G _V) . (() . x0) = () . y & (G _V) . (() . x0) = () . y ) or ( (G _V) . (() . x0) = () . y & (G _V) . (() . x0) = () . y ) ) by ;
then A33: (G _E) . x Joins () . y,() . y,G2 by ;
A34: (G _E) . x in the_Edges_of G2 by ;
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 & () . y = w2 ) or ( () . y = w2 & () . y = w1 ) ) by ;
then A37: ( y = e & h . ((G _E) . x) = e ) by ;
A38: x in dom (h * (G _E)) by ;
then A39: x in dom ((h * (G _E)) | E1) by ;
y = (h * (G _E)) . x by
.= ((h * (G _E)) | E1) . x by ;
hence y in rng ((h * (G _E)) | E1) by ; :: thesis: verum
end;
then A40: rng ((h * (G _E)) | E1) = E2 by TARSKI:2;
then reconsider g = (h * (G _E)) | E1 as PartFunc of (),() by ;
now :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . 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 ( () . e in dom f & () . e in dom f ) )
set v = () . e;
set w = () . e;
assume e in dom g ; :: thesis: ( () . e in dom f & () . e in dom f )
then e Joins () . e,() . e,G3 by GLIB_000:def 13;
then ( (the_Source_of G3) . e in the_Vertices_of G3 & () . e in the_Vertices_of G3 ) by GLIB_000:13;
then ( (the_Source_of G3) . e in the_Vertices_of G1 & () . e in the_Vertices_of G1 ) ;
hence ( (the_Source_of G3) . e in dom f & () . e in dom f ) by ; :: 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 ;
then A45: (G _E) . e Joins f . v,f . w,G2 by ;
A46: ( h . ((G _E) . e) in E2 & [((G _E) . e),(h . ((G _E) . e))] in EdgeAdjEqRel G2 ) by ;
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 ;
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 ; :: thesis: verum
end;
end;
end;
then A48: h . ((G _E) . e) Joins f . v,f . w,G4 by ;
g . e = (h * (G _E)) . e by
.= h . ((G _E) . e) by ;
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 ;
then A49: F is total by ;
rng f = the_Vertices_of G4 by ;
then A50: F is onto by ;
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 ;
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 ;
then ( (the_Source_of G2) . ((G _E) . x1) in rng (G _V) & () . ((G _E) . x1) in rng (G _V) ) by Th6;
then A56: ( v1 in rng (G _V) & v2 in rng (G _V) ) by ;
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 ;
A59: x1 Joins u1,u2,G1 by A1, A53, A55, A57, A58, Def15;
h . ((G _E) . x1) = (h * (G _E)) . x1 by
.= g . x2 by
.= (h * (G _E)) . x2 by
.= h . ((G _E) . x2) by ;
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 ;
(G _E) . x2 Joins v1,v2,G2
proof
per cases ( ( v1 = w1 & v2 = w2 ) or ( v1 = w2 & v2 = w1 ) ) by ;
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 ; :: 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 ;
hence G4 is G3 -isomorphic by ; :: thesis: verum