let G be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1, G2 be addAdjVertexAll of G,v,V; :: thesis:

per cases ;

suppose A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis:

defpred S₁[ object , object ] means for v1, v2 being object st $1 Joins v1,v2,G1 holds
$2 Joins v1,v2,G2;
A2: for e1 being object st e1 in the_Edges_of G1 holds
ex e2 being object st
( e2 in the_Edges_of G2 & S₁[e1,e2] )

proof

let e1 be object ; :: thesis:
assume e1 in the_Edges_of G1 ; :: thesis:
then e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 by GLIB_000:def 13;
then consider e2 being object such that
A3: e2 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G2 by Th67;
take e2 ; :: thesis:
thus e2 in the_Edges_of G2 by A3, GLIB_000:def 13; :: thesis:
let v1, v2 be object ; :: thesis:
assume e1 Joins v1,v2,G1 ; :: thesis:

per cases ) . e1 = v1 & (the_Target_of G1) . e1 = v2 ) or ( (the_Source_of G1) . e1 = v2 & (the_Target_of G1) . e1 = v1 ) ) by GLIB_000:def 13;

suppose ( (the_Source_of G1) . e1 = v1 & (the_Target_of G1) . e1 = v2 ) ; :: thesis:

hence e2 Joins v1,v2,G2 by A3; :: thesis:

end;

suppose ( (the_Source_of G1) . e1 = v2 & (the_Target_of G1) . e1 = v1 ) ; :: thesis:

hence e2 Joins v1,v2,G2 by A3, GLIB_000:14; :: thesis:

end;

consider f1 being Function of (the_Edges_of G1),(the_Edges_of G2) such that
A4: for e1 being object st e1 in the_Edges_of G1 holds
S₁[e1,f1 . e1] from FUNCT_2:sch 1(A2);
set f = f1 +* (id (the_Edges_of G));
A5: the_Edges_of G c= the_Edges_of G1 by GLIB_006:def 9;
A6: dom f1 = the_Edges_of G1

proof

per cases ;

suppose V <> {} ; :: thesis:

then the_Edges_of G2 <> {} by A1, Th47;
hence dom f1 = the_Edges_of G1 by FUNCT_2:def 1; :: thesis:

end;

suppose A7: the_Edges_of G <> {} ; :: thesis:

the_Edges_of G2 <> {}

proof

assume A8: the_Edges_of G2 = {} ; :: thesis:
the_Edges_of G c= the_Edges_of G2 by GLIB_006:def 9;
hence contradiction by A7, A8; :: thesis:

end;

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

end;

suppose ( V = {} & the_Edges_of G = {} ) ; :: thesis:

then ( the_Edges_of G1 = {} & the_Edges_of G2 = {} ) by Lm11;
hence dom f1 = the_Edges_of G1 ; :: thesis:

end;

A9: dom (f1 +* (id (the_Edges_of G))) = (dom f1) \/ (dom (id (the_Edges_of G))) by FUNCT_4:def 1
.= the_Edges_of G1 by A5, A6, XBOOLE_1:12 ;
A10: rng (id (the_Edges_of G)) c= the_Edges_of G2 by GLIB_006:def 9;
A11: (rng f1) \/ (rng (id (the_Edges_of G))) c= the_Edges_of G2 by A10, XBOOLE_1:8;
rng (f1 +* (id (the_Edges_of G))) c= (rng f1) \/ (rng (id (the_Edges_of G))) by FUNCT_4:17;
then reconsider f = f1 +* (id (the_Edges_of G)) as Function of (the_Edges_of G1),(the_Edges_of G2) by A9, FUNCT_2:2, A11, XBOOLE_1:1;
take f ; :: thesis:
thus f | (the_Edges_of G) = f | (dom (id (the_Edges_of G)))
.= id (the_Edges_of G) ; :: thesis:
consider E1 being set such that
card V = card E1 and
A12: ( E1 misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E1 ) and
A13: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E1 & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
consider E2 being set such that
card V = card E2 and
A14: ( E2 misses the_Edges_of G & the_Edges_of G2 = (the_Edges_of G) \/ E2 ) and
A15: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E2 & e1 Joins v1,v,G2 & ( for e2 being object st e2 Joins v1,v,G2 holds
e1 = e2 ) ) by A1, Def4;
for e1, e2 being object st e1 in dom f & e2 in dom f & f . e1 = f . e2 holds
e1 = e2

proof

let e1, e2 be object ; :: thesis:
assume that
A16: ( e1 in dom f & e2 in dom f ) and
A17: f . e1 = f . e2 ; :: thesis:
set x1 = (the_Source_of G1) . e1;
set y1 = (the_Target_of G1) . e1;
set x2 = (the_Source_of G1) . e2;
set y2 = (the_Target_of G1) . e2;
A18: ( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 ) by A16;

per cases ;

suppose A19: ( e1 in the_Edges_of G & e2 in the_Edges_of G ) ; :: thesis:

then ( e1 in dom (id (the_Edges_of G)) & e2 in dom (id (the_Edges_of G)) ) ;
then ( f . e1 = (id (the_Edges_of G)) . e1 & f . e2 = (id (the_Edges_of G)) . e2 ) by FUNCT_4:13;
then ( f . e1 = e1 & f . e2 = e2 ) by A19, FUNCT_1:18;
hence e1 = e2 by A17; :: thesis:

end;

suppose A20: ( not e1 in the_Edges_of G & e2 in the_Edges_of G ) ; :: thesis:

then ( not e1 in dom (id (the_Edges_of G)) & e2 in dom (id (the_Edges_of G)) ) ;
then A21: ( f . e1 = f1 . e1 & f . e2 = (id (the_Edges_of G)) . e2 ) by FUNCT_4:11, FUNCT_4:13;
A22: e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 by A18, GLIB_000:def 13;
then A23: ( not (the_Source_of G1) . e1 in the_Vertices_of G or not (the_Target_of G1) . e1 in the_Vertices_of G ) by A1, A12, A20, Th51;
e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G1 by A18, GLIB_000:def 13;
then A24: e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G by A20, GLIB_006:72;
then A25: ( (the_Source_of G1) . e2 in the_Vertices_of G & (the_Target_of G1) . e2 in the_Vertices_of G ) by GLIB_000:13;
A26: f . e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G2 by A21, A18, A22, A4;
A27: e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G2 by A24, GLIB_006:70;
f . e2 = e2 by A20, A21, FUNCT_1:18;
hence e1 = e2 by A23, A25, A26, GLIB_000:15, A17, A27; :: thesis:

end;

suppose A28: ( not e2 in the_Edges_of G & e1 in the_Edges_of G ) ; :: thesis:

end;

suppose A36: ( not e1 in the_Edges_of G & not e2 in the_Edges_of G ) ; :: thesis:

then ( not e1 in dom (id (the_Edges_of G)) & not e2 in dom (id (the_Edges_of G)) ) ;
then A37: ( f . e1 = f1 . e1 & f . e2 = f1 . e2 ) by FUNCT_4:11;
A38: e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G1 by A18, GLIB_000:def 13;
then A39: ( e1 in E1 & ( ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 in V ) or ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) ) ) by A1, A12, A36, Th51;
A40: e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G1 by A18, GLIB_000:def 13;
A41: f . e1 Joins (the_Source_of G1) . e1,(the_Target_of G1) . e1,G2 by A18, A38, A37, A4;
f . e2 Joins (the_Source_of G1) . e2,(the_Target_of G1) . e2,G2 by A18, A40, A37, A4;

per cases ) . e1 = (the_Source_of G1) . e2 & (the_Target_of G1) . e1 = (the_Target_of G1) . e2 ) or ( (the_Source_of G1) . e1 = (the_Target_of G1) . e2 & (the_Target_of G1) . e1 = (the_Source_of G1) . e2 ) ) by A17, A41, GLIB_000:15;

suppose A42: ( (the_Source_of G1) . e1 = (the_Source_of G1) . e2 & (the_Target_of G1) . e1 = (the_Target_of G1) . e2 ) ; :: thesis:

per cases ) . e1 = v & (the_Target_of G1) . e1 in V ) or ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) ) by A39;

suppose A43: ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 in V ) ; :: thesis:

then consider e being object such that
( e in E1 & e Joins (the_Target_of G1) . e1,v,G1 ) and
A44: for e3 being object st e3 Joins (the_Target_of G1) . e1,v,G1 holds
e = e3 by A13;
e1 = e by A44, A38, A43, GLIB_000:14;
hence e1 = e2 by A44, A40, A42, A43, GLIB_000:14; :: thesis:

end;

suppose A46: ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) ; :: thesis:

then consider e being object such that
( e in E1 & e Joins (the_Source_of G1) . e1,v,G1 ) and
A47: for e3 being object st e3 Joins (the_Source_of G1) . e1,v,G1 holds
e = e3 by A13;
e1 Joins (the_Source_of G1) . e1,v,G1 by A38, A46;
then e1 = e by A47;
hence e1 = e2 by A47, A40, A42, A46; :: thesis:

end;

suppose A49: ( (the_Source_of G1) . e1 = (the_Target_of G1) . e2 & (the_Target_of G1) . e1 = (the_Source_of G1) . e2 ) ; :: thesis:

per cases ) . e1 = v & (the_Target_of G1) . e1 in V ) or ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) ) by A39;

suppose A50: ( (the_Source_of G1) . e1 = v & (the_Target_of G1) . e1 in V ) ; :: thesis:

then consider e being object such that
( e in E1 & e Joins (the_Target_of G1) . e1,v,G1 ) and
A51: for e3 being object st e3 Joins (the_Target_of G1) . e1,v,G1 holds
e = e3 by A13;
e1 = e by A51, A38, A50, GLIB_000:14;
hence e1 = e2 by A51, A40, A49, A50; :: thesis:

end;

suppose A53: ( (the_Target_of G1) . e1 = v & (the_Source_of G1) . e1 in V ) ; :: thesis:

then consider e being object such that
( e in E1 & e Joins (the_Source_of G1) . e1,v,G1 ) and
A54: for e3 being object st e3 Joins (the_Source_of G1) . e1,v,G1 holds
e = e3 by A13;
e1 Joins (the_Source_of G1) . e1,v,G1 by A38, A53;
then A55: e1 = e by A54;
e2 Joins (the_Source_of G1) . e1,v,G1 by A40, A49, A53, GLIB_000:14;
hence e1 = e2 by A54, A55; :: thesis:

end;

hence f is one-to-one by FUNCT_1:def 4; :: thesis:
for e being object st e in the_Edges_of G2 holds
e in rng f

proof

let e be object ; :: thesis:
assume A56: e in the_Edges_of G2 ; :: thesis:

per cases ;

suppose A57: e in the_Edges_of G ; :: thesis:

then e in dom (id (the_Edges_of G)) ;
then A58: f . e = (id (the_Edges_of G)) . e by FUNCT_4:13
.= e by A57, FUNCT_1:18 ;
the_Edges_of G c= the_Edges_of G1 by GLIB_006:def 9;
hence e in rng f by A58, FUNCT_1:def 3, A9, A57; :: thesis:

end;

suppose A59: not e in the_Edges_of G ; :: thesis:

set v1 = (the_Source_of G2) . e;
set v2 = (the_Target_of G2) . e;
A60: e Joins (the_Source_of G2) . e,(the_Target_of G2) . e,G2 by A56, GLIB_000:def 13;

per cases ) . e = v & (the_Target_of G2) . e in V ) or ( (the_Target_of G2) . e = v & (the_Source_of G2) . e in V ) ) by A1, A14, A59, Th51;

suppose A61: ( (the_Source_of G2) . e = v & (the_Target_of G2) . e in V ) ; :: thesis:

then consider e1 being object such that
A62: ( e1 in E1 & e1 Joins (the_Target_of G2) . e,v,G1 ) and
for e2 being object st e2 Joins (the_Target_of G2) . e,v,G1 holds
e1 = e2 by A13;
A63: e1 in the_Edges_of G1 by A62, GLIB_000:def 13;
then A64: f1 . e1 Joins (the_Target_of G2) . e,v,G2 by A62, A4;
E1 /\ (the_Edges_of G) = {} by A12, XBOOLE_0:def 7;
then not e1 in dom (id (the_Edges_of G)) by A62, Lm7;
then A65: f . e1 Joins (the_Target_of G2) . e,v,G2 by A64, FUNCT_4:11;
consider e3 being object such that
( e3 in E2 & e3 Joins (the_Target_of G2) . e,v,G2 ) and
A66: for e2 being object st e2 Joins (the_Target_of G2) . e,v,G2 holds
e3 = e2 by A15, A61;
f . e1 = e3 by A65, A66;
then f . e1 = e by A66, A61, A60, GLIB_000:14;
hence e in rng f by A63, A9, FUNCT_1:def 3; :: thesis:

end;

suppose A68: ( (the_Target_of G2) . e = v & (the_Source_of G2) . e in V ) ; :: thesis:

then consider e1 being object such that
A69: ( e1 in E1 & e1 Joins (the_Source_of G2) . e,v,G1 ) and
for e2 being object st e2 Joins (the_Source_of G2) . e,v,G1 holds
e1 = e2 by A13;
A70: e1 in the_Edges_of G1 by A69, GLIB_000:def 13;
then A71: f1 . e1 Joins (the_Source_of G2) . e,v,G2 by A69, A4;
E1 /\ (the_Edges_of G) = {} by A12, XBOOLE_0:def 7;
then not e1 in dom (id (the_Edges_of G)) by A69, Lm7;
then A72: f . e1 Joins (the_Source_of G2) . e,v,G2 by A71, FUNCT_4:11;
consider e3 being object such that
( e3 in E2 & e3 Joins (the_Source_of G2) . e,v,G2 ) and
A73: for e2 being object st e2 Joins (the_Source_of G2) . e,v,G2 holds
e3 = e2 by A15, A68;
f . e1 = e3 by A72, A73;
then f . e1 = e by A73, A68, A60;
hence e in rng f by A70, A9, FUNCT_1:def 3; :: thesis:

end;

then the_Edges_of G2 c= rng f by TARSKI:def 3;
hence f is onto by FUNCT_2:def 3, XBOOLE_0:def 10; :: thesis:
let v1, e, v2 be object ; :: thesis:
assume A75: e Joins v1,v2,G1 ; :: thesis:

per cases ;

suppose A76: e in the_Edges_of G ; :: thesis:

then e in dom (id (the_Edges_of G)) ;
then A77: f . e = (id (the_Edges_of G)) . e by FUNCT_4:13
.= e by A76, FUNCT_1:18 ;
reconsider w1 = v1, w2 = v2 as set by TARSKI:1;
e Joins w1,w2,G by A75, A76, GLIB_006:72;
hence f . e Joins v1,v2,G2 by A77, GLIB_006:70; :: thesis:

end;

suppose not e in the_Edges_of G ; :: thesis:

then not e in dom (id (the_Edges_of G)) ;
then A78: f . e = f1 . e by FUNCT_4:11;
e in the_Edges_of G1 by A75, GLIB_000:def 13;
hence f . e Joins v1,v2,G2 by A78, A75, A4; :: thesis:

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis:

then A79: ( G1 == G & G2 == G ) by Def4;
then A80: ( the_Edges_of G1 = the_Edges_of G & the_Edges_of G2 = the_Edges_of G ) by GLIB_000:def 34;
set f = id (the_Edges_of G);
reconsider f = id (the_Edges_of G) as Function of (the_Edges_of G1),(the_Edges_of G2) by A80;
take f ; :: thesis:
thus f | (the_Edges_of G) = id (the_Edges_of G) ; :: thesis:
thus ( f is one-to-one & f is onto ) by A80; :: thesis:
let v1, e, v2 be object ; :: thesis:
assume A81: e Joins v1,v2,G1 ; :: thesis:
G1 == G2 by A79, GLIB_000:85;
then A82: e Joins v1,v2,G2 by A81, GLIB_000:88;
e in the_Edges_of G1 by A81, GLIB_000:def 13;
hence f . e Joins v1,v2,G2 by A80, A82, FUNCT_1:18; :: thesis:

end;