let G2 be _Graph; for v being object
for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
let v be object ; for V being set
for G1 being addAdjVertexAll of G2,v,V
for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
let V be set ; for G1 being addAdjVertexAll of G2,v,V
for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
let G1 be addAdjVertexAll of G2,v,V; for E being set st V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 holds
ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
let E be set ; ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & E misses the_Edges_of G2 implies ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) ) )
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 )
; ex f, g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
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 S1[ 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} & S1[e,v1] )
proof
let e be
object ;
( e in E implies ex v1 being object st
( v1 in V \/ {v} & S1[e,v1] ) )
set x =
(the_Source_of G1) . e;
set y =
(the_Target_of G1) . e;
assume A8:
e in E
;
ex v1 being object st
( v1 in V \/ {v} & S1[e,v1] )
then A9:
not
e in the_Edges_of G2
by A5, A6, Lm7;
take
(the_Source_of G1) . e
;
( (the_Source_of G1) . e in V \/ {v} & S1[e,(the_Source_of G1) . e] )
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;
S1[e,(the_Source_of G1) . e]
take
(the_Target_of G1) . e
;
e DJoins (the_Source_of G1) . e,(the_Target_of G1) . e,G1
thus
e DJoins (the_Source_of G1) . e,
(the_Target_of G1) . e,
G1
by A10, GLIB_000:def 14;
verum
end;
consider f being Function of E,(V \/ {v}) such that
A11:
for e being object st e in E holds
S1[e,f . e]
from FUNCT_2:sch 1(A7);
defpred S2[ 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} & S2[e,v2] )
proof
let e be
object ;
( e in E implies ex v2 being object st
( v2 in V \/ {v} & S2[e,v2] ) )
assume A13:
e in E
;
ex v2 being object st
( v2 in V \/ {v} & S2[e,v2] )
then consider v2 being
object such that A14:
e DJoins f . e,
v2,
G1
by A11;
take
v2
;
( v2 in V \/ {v} & S2[e,v2] )
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;
S2[e,v2]
thus
S2[
e,
v2]
by A14;
verum
end;
consider g being Function of E,(V \/ {v}) such that
A16:
for e being object st e in E holds
S2[e,g . e]
from FUNCT_2:sch 1(A12);
take
f
; ex g being Function of E,(V \/ {v}) st
( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
take
g
; ( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
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
hence
the_Source_of G1 = (the_Source_of G2) +* f
by A17, FUNCT_1:2; ( the_Target_of G1 = (the_Target_of G2) +* g & ( for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) ) )
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
hence
the_Target_of G1 = (the_Target_of G2) +* g
by A21, FUNCT_1:2; for e being object st e in E holds
( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) )
let e be object ; ( e in E implies ( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) ) )
assume A25:
e in E
; ( e DJoins f . e,g . e,G1 & ( f . e = v implies g . e <> v ) & ( g . e <> v implies f . e = v ) )
hence A26:
e DJoins f . e,g . e,G1
by A16; ( f . e = v iff g . e <> v )
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; ( g . e <> v implies f . e = v )
assume A28:
g . e <> v
; f . e = v
assume
f . e <> v
; contradiction
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; verum