let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
let E be set ; :: thesis:
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: ( the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 ) ; :: thesis:
consider E1 being set such that
A3: ( card V = card E1 & E1 misses the_Edges_of G2 ) and
A4: the_Edges_of G1 = (the_Edges_of G2) \/ 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 e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
A5: E1 /\ (the_Edges_of G2) = {} by A3, XBOOLE_0:def 7;
A6: E = E1 by A2, A3, A4, XBOOLE_1:71;
defpred S₁[ object , object ] means ex v2 being object st $1 DJoins $2,v2,G1;
A7: for e being object st e in E holds
ex v1 being object st
( v1 in V \/ {v} & S₁[e,v1] )

proof

let e be object ; :: thesis:
set x = (the_Source_of G1) . e;
set y = (the_Target_of G1) . e;
assume A8: e in E ; :: thesis:
then A9: not e in the_Edges_of G2 by A5, A6, Lm7;
take (the_Source_of G1) . e ; :: thesis:
A10: e in the_Edges_of G1 by A8, A4, A6, XBOOLE_0:def 3;
then e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by GLIB_000:def 13;
then ( (the_Source_of G1) . e = v or (the_Source_of G1) . e in V ) by A1, A3, A4, A9, Th51;
then ( (the_Source_of G1) . e in {v} or (the_Source_of G1) . e in V ) by TARSKI:def 1;
hence (the_Source_of G1) . e in V \/ {v} by XBOOLE_0:def 3; :: thesis:
take (the_Target_of G1) . e ; :: thesis:
thus e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A10, GLIB_000:def 14; :: thesis:

end;

consider f being Function of E,(V \/ {v}) such that
A11: for e being object st e in E holds
S₁[e,f . e] from FUNCT_2:sch 1(A7);
defpred S₂[ object , object ] means $1 DJoins f . $1,$2,G1;
A12: for e being object st e in E holds
ex v2 being object st
( v2 in V \/ {v} & S₂[e,v2] )

proof

let e be object ; :: thesis:
assume A13: e in E ; :: thesis:
then consider v2 being object such that
A14: e DJoins f . e,v2,G1 by A11;
take v2 ; :: thesis:
A15: not e in the_Edges_of G2 by A5, A6, A13, Lm7;
e Joins f . e,v2,G1 by A14, GLIB_000:16;
then ( v2 = v or v2 in V ) by A1, A3, A4, A15, Th51;
then ( v2 in {v} or v2 in V ) by TARSKI:def 1;
hence v2 in V \/ {v} by XBOOLE_0:def 3; :: thesis:
thus S₂[e,v2] by A14; :: thesis:

end;

consider g being Function of E,(V \/ {v}) such that
A16: for e being object st e in E holds
S₂[e,g . e] from FUNCT_2:sch 1(A12);
take f ; :: thesis:
take g ; :: thesis:
A17: dom ((the_Source_of G2) +* f) = (dom (the_Source_of G2)) \/ (dom f) by FUNCT_4:def 1
.= (the_Edges_of G2) \/ (dom f) by GLIB_000:4
.= (the_Edges_of G2) \/ E by FUNCT_2:def 1
.= dom (the_Source_of G1) by A2, GLIB_000:4 ;
for e being object st e in dom (the_Source_of G1) holds
(the_Source_of G1) . e = ((the_Source_of G2) +* f) . e

proof

let e be object ; :: thesis:
assume e in dom (the_Source_of G1) ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

suppose A18: e in the_Edges_of G2 ; :: thesis:

then not e in dom f by A5, A6, Lm7;
then ((the_Source_of G2) +* f) . e = (the_Source_of G2) . e by FUNCT_4:11
.= (the_Source_of G1) . e by A18, GLIB_006:def 9 ;
hence (the_Source_of G1) . e = ((the_Source_of G2) +* f) . e ; :: thesis:

end;

suppose A19: e in E ; :: thesis:

then e in dom f by FUNCT_2:def 1;
then A20: ((the_Source_of G2) +* f) . e = f . e by FUNCT_4:13;
e DJoins f . e,g . e,G1 by A16, A19;
hence (the_Source_of G1) . e = ((the_Source_of G2) +* f) . e by A20, GLIB_000:def 14; :: thesis:

end;

end;

end;

hence the_Source_of G1 = (the_Source_of G2) +* f by A17, FUNCT_1:2; :: thesis:
A21: dom ((the_Target_of G2) +* g) = (dom (the_Target_of G2)) \/ (dom g) by FUNCT_4:def 1
.= (the_Edges_of G2) \/ (dom g) by GLIB_000:4
.= (the_Edges_of G2) \/ E by FUNCT_2:def 1
.= dom (the_Target_of G1) by A2, GLIB_000:4 ;
for e being object st e in dom (the_Target_of G1) holds
(the_Target_of G1) . e = ((the_Target_of G2) +* g) . e

proof

let e be object ; :: thesis:
assume e in dom (the_Target_of G1) ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

suppose A22: e in the_Edges_of G2 ; :: thesis:

then not e in dom g by A5, A6, Lm7;
then ((the_Target_of G2) +* g) . e = (the_Target_of G2) . e by FUNCT_4:11
.= (the_Target_of G1) . e by A22, GLIB_006:def 9 ;
hence (the_Target_of G1) . e = ((the_Target_of G2) +* g) . e ; :: thesis:

end;

suppose A23: e in E ; :: thesis:

then e in dom g by FUNCT_2:def 1;
then A24: ((the_Target_of G2) +* g) . e = g . e by FUNCT_4:13;
e DJoins f . e,g . e,G1 by A16, A23;
hence (the_Target_of G1) . e = ((the_Target_of G2) +* g) . e by A24, GLIB_000:def 14; :: thesis:

end;

end;

end;

hence the_Target_of G1 = (the_Target_of G2) +* g by A21, FUNCT_1:2; :: thesis:
let e be object ; :: thesis:
assume A25: e in E ; :: thesis:
hence A26: e DJoins f . e,g . e,G1 by A16; :: thesis:
then A27: e Joins f . e,g . e,G1 by GLIB_000:16;
thus ( f . e = v implies g . e <> v ) by A1, A27, Def4; :: thesis:
assume A28: g . e <> v ; :: thesis:
assume f . e <> v ; :: thesis:
then e DJoins f . e,g . e,G2 by A1, A26, A28, Def4;
then e in the_Edges_of G2 by GLIB_000:def 14;
hence contradiction by A25, A5, A6, Lm7; :: thesis: