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

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

end;

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

reconsider g = g as PartFunc of (the_Edges_of G1),(the_Edges_of G2) ;

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

A11:
rng g = the_Edges_of G2
by A3, FUNCT_2:def 3;per cases
( the_Edges_of G2 <> {} or the_Edges_of G2 = {} )
;

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

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

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;( (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, 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 )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;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

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

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

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