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 (() \/ {v});
consider E1 being set such that
A2: ( card V = card E1 & E1 misses the_Edges_of G & the_Edges_of G1 = () \/ 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 ;
consider g being Function of (),() such that
A3: ( g | () = id () & 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 (() \/ {v})) = the_Vertices_of G1 by ;
A6: rng (id (() \/ {v})) = the_Vertices_of G2 by ;
reconsider f = id (() \/ {v}) as PartFunc of (),() by A5, A6;
A7: dom g = the_Edges_of G1 A11: rng g = the_Edges_of G2 by ;
reconsider g = g as PartFunc of (),() ;
now :: thesis: ( ( for e being object st e in dom g holds
( () . e in dom f & () . 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 ( () . e in dom f & () . e in dom f ) )
assume e in dom g ; :: thesis: ( () . e in dom f & () . e in dom f )
then e Joins () . e,() . e,G1 by GLIB_000:def 13;
hence ( (the_Source_of G1) . e in dom f & () . e in dom f ) by ; :: 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 () \/ {v} & w in () \/ {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 ;
hence g . e Joins f . v0,f . w,G2 by ; :: 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 ;
hence G2 is G1 -isomorphic by ; :: thesis: verum
end;
suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: G2 is G1 -isomorphic
end;
end;