let G be finite Graph; for v being Vertex of G
for vs being FinSequence of the carrier of G
for c being Path of G st not c is cyclic & vs is_vertex_seq_of c holds
( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )
let v be Vertex of G; for vs being FinSequence of the carrier of G
for c being Path of G st not c is cyclic & vs is_vertex_seq_of c holds
( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )
let vs be FinSequence of the carrier of G; for c being Path of G st not c is cyclic & vs is_vertex_seq_of c holds
( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )
let c be Path of G; ( not c is cyclic & vs is_vertex_seq_of c implies ( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) ) )
assume that
A1:
not c is cyclic
and
A2:
vs is_vertex_seq_of c
; ( Degree (v,(rng c)) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )
len vs = (len c) + 1
by A2;
then A3:
1 <= len vs
by NAT_1:11;
then
( 1 in dom vs & len vs in dom vs )
by FINSEQ_3:25;
then reconsider v1 = vs . 1, v2 = vs . (len vs) as Vertex of G by FINSEQ_2:11;
A4:
v1 <> v2
by A1, A2;
set G9 = AddNewEdge (v1,v2);
reconsider vs9 = vs as FinSequence of the carrier of (AddNewEdge (v1,v2)) by Def7;
reconsider c9 = c as Path of AddNewEdge (v1,v2) by Th37;
A5:
vs9 is_vertex_seq_of c9
by A2, Th36;
reconsider v9 = v, v19 = v1, v29 = v2 as Vertex of (AddNewEdge (v1,v2)) by Def7;
set v219 = <*v29,v19*>;
set vs9e = vs9 ^' <*v29,v19*>;
len <*v29,v19*> = 2
by FINSEQ_1:44;
then A6:
(vs9 ^' <*v29,v19*>) . (len (vs9 ^' <*v29,v19*>)) = <*v29,v19*> . 2
by FINSEQ_6:142;
set E = the carrier' of G;
set e = the carrier' of G;
A7:
the carrier' of G in { the carrier' of G}
by TARSKI:def 1;
the carrier' of (AddNewEdge (v1,v2)) = the carrier' of G \/ { the carrier' of G}
by Def7;
then
the carrier' of G in the carrier' of (AddNewEdge (v1,v2))
by A7, XBOOLE_0:def 3;
then reconsider ep = <* the carrier' of G*> as Path of AddNewEdge (v1,v2) by Th4;
A8:
rng ep = { the carrier' of G}
by FINSEQ_1:39;
A9:
not the carrier' of G in the carrier' of G
;
then
rng ep misses the carrier' of G
by A8, ZFMISC_1:50;
then A10:
(rng ep) /\ the carrier' of G = {}
;
( the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v19 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v29 )
by Th34;
then A11:
( vs9 . (len vs9) = <*v29,v19*> . 1 & <*v29,v19*> is_vertex_seq_of ep )
by Th11, FINSEQ_1:44;
A12:
rng c c= the carrier' of G
by FINSEQ_1:def 4;
then A13:
not the carrier' of G in rng c
by A9;
rng c9 misses rng ep
then reconsider c9e = c9 ^ ep as Path of AddNewEdge (v1,v2) by A5, A11, Th6;
A14:
vs9 ^' <*v29,v19*> is_vertex_seq_of c9e
by A5, A11, GRAPH_2:44;
(vs9 ^' <*v29,v19*>) . 1 = vs . 1
by A3, FINSEQ_6:140;
then
(vs9 ^' <*v29,v19*>) . 1 = (vs9 ^' <*v29,v19*>) . (len (vs9 ^' <*v29,v19*>))
by A6, FINSEQ_1:44;
then reconsider c9e = c9e as cyclic Path of AddNewEdge (v1,v2) by A14, MSSCYC_1:def 2;
rng c9e = (rng c) \/ (rng ep)
by FINSEQ_1:31;
then A15:
the carrier' of G in rng c9e
by A7, A8, XBOOLE_0:def 3;
A16: (rng c9e) /\ the carrier' of G =
((rng c) \/ (rng ep)) /\ the carrier' of G
by FINSEQ_1:31
.=
((rng c) /\ the carrier' of G) \/ {}
by A10, XBOOLE_1:23
.=
rng c
by A12, XBOOLE_1:28
;
then A17:
Degree (v,(rng c9e)) = Degree (v,(rng c))
by Th31;
reconsider dv9 = Degree (v9,(rng c9e)) as even Element of NAT by Th49;
A18:
Degree (v9,(rng c9e)) is even
by Th49;