let G be _Graph; :: thesis: for v being object
for V being set
for G1, G2 being addAdjVertexAll of G,v,V holds G2 is G1 -isomorphic
let v be object ; :: thesis: for V being set
for G1, G2 being addAdjVertexAll of G,v,V holds G2 is G1 -isomorphic
let V be set ; :: thesis: for G1, G2 being addAdjVertexAll of G,v,V holds G2 is G1 -isomorphic
let G1, G2 be addAdjVertexAll of G,v,V; :: thesis: G2 is G1 -isomorphic

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: G2 is G1 -isomorphic

set f = id ((the_Vertices_of G) \/ {v});
consider E1 being set such that
A2: ( card V = card E1 & E1 misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E1 ) and
for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E1 & e1 Joins v1,v,G1 & ( for e9 being object st e9 Joins v1,v,G1 holds
e1 = e9 ) ) by A1, GLIB_007:def 4;
consider g being Function of (the_Edges_of G1),(the_Edges_of G2) such that
A3: ( g | (the_Edges_of G) = id (the_Edges_of G) & g is one-to-one & g is onto ) and
A4: for v1, e, v2 being object st e Joins v1,v2,G1 holds
g . e Joins v1,v2,G2 by GLIB_007:68;
A5: dom (id ((the_Vertices_of G) \/ {v})) = the_Vertices_of G1 by A1, GLIB_007:def 4;
A6: rng (id ((the_Vertices_of G) \/ {v})) = the_Vertices_of G2 by A1, GLIB_007:def 4;
reconsider f = id ((the_Vertices_of G) \/ {v}) as PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) by A5, A6;
A7: dom g = the_Edges_of G1

proof

per cases ( the_Edges_of G2 <> {} or the_Edges_of G2 = {} ) ;

suppose the_Edges_of G2 <> {} ; :: thesis: dom g = the_Edges_of G1

hence dom g = the_Edges_of G1 by FUNCT_2:def 1; :: thesis: verum

end;

suppose A8: the_Edges_of G2 = {} ; :: thesis: dom g = the_Edges_of G1

the_Edges_of G c= the_Edges_of G2 by GLIB_006:def 9;
then A9: the_Edges_of G = {} by A8, XBOOLE_1:3;
V is empty by A1, A8, GLIB_007:47;
then A10: ( card (the_Edges_of G) = 0 & card E1 = 0 ) by A2, A9;
card (the_Edges_of G1) = (card (the_Edges_of G)) +` (card E1) by A2, CARD_2:35
.= 0 by A10, CARD_2:18 ;
then the_Edges_of G1 = {} ;
hence dom g = the_Edges_of G1 ; :: thesis: verum

end;

end;

end;

A11: rng g = the_Edges_of G2 by A3, FUNCT_2:def 3;
reconsider g = g as PartFunc of (the_Edges_of G1),(the_Edges_of G2) ;

now :: thesis: ( ( for e being object st e in dom g holds
( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) ) & ( for e, v0, w being object st e in dom g & v0 in dom f & w in dom f & e Joins v0,w,G1 holds
g . e Joins f . v0,f . w,G2 ) )

hereby :: thesis: for e, v0, w being object st e in dom g & v0 in dom f & w in dom f & e Joins v0,w,G1 holds
g . e Joins f . v0,f . w,G2

let e be object ; :: thesis: ( e in dom g implies ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) )
assume e in dom g ; :: thesis: ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f )
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;
hence ( (the_Source_of G1) . e in dom f & (the_Target_of G1) . e in dom f ) by A5, GLIB_000:13; :: thesis: verum

end;

let e, v0, w be object ; :: thesis: ( e in dom g & v0 in dom f & w in dom f & e Joins v0,w,G1 implies g . e Joins f . v0,f . w,G2 )
assume ( e in dom g & v0 in dom f & w in dom f ) ; :: thesis: ( e Joins v0,w,G1 implies g . e Joins f . v0,f . w,G2 )
then A12: ( v0 in (the_Vertices_of G) \/ {v} & w in (the_Vertices_of G) \/ {v} ) ;
assume e Joins v0,w,G1 ; :: thesis: g . e Joins f . v0,f . w,G2
then g . e Joins v0,w,G2 by A4;
then g . e Joins f . v0,w,G2 by A12, FUNCT_1:18;
hence g . e Joins f . v0,f . w,G2 by A12, FUNCT_1:18; :: thesis: verum

end;

then reconsider F = [f,g] as PGraphMapping of G1,G2 by Th8;
A13: F is total by A5, A7;
A14: F is one-to-one by A3;
F is onto by A6, A11;
hence G2 is G1 -isomorphic by A13, A14; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G2 is G1 -isomorphic

then ( G1 == G & G2 == G ) by GLIB_007:def 4;
then A15: ( G1 is reverseEdgeDirections of G, {} & G2 is reverseEdgeDirections of G, {} ) by GLIB_009:42;
G is G -isomorphic by Th53;
hence G2 is G1 -isomorphic by A15, Th143; :: thesis: verum

end;

end;