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, GRAPH_2:def 7;
then A3:
1 <= len vs
by NAT_1:11;
then
( 1 in dom vs & len vs in dom vs )
by FINSEQ_3:27;
then reconsider v1 = vs . 1, v2 = vs . (len vs) as Vertex of G by FINSEQ_2:13;
A4:
v1 <> v2
by A1, A2, MSSCYC_1:def 2;
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 Th42;
A5:
vs9 is_vertex_seq_of c9
by A2, Th41;
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:61;
then A6:
(vs9 ^' <*v29,v19*>) . (len (vs9 ^' <*v29,v19*>)) = <*v29,v19*> . 2
by GRAPH_2:16;
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 Th7;
A8:
rng ep = {the carrier' of G}
by FINSEQ_1:56;
A9:
not the carrier' of G in the carrier' of G
;
then
rng ep misses the carrier' of G
by A8, ZFMISC_1:56;
then A10:
(rng ep) /\ the carrier' of G = {}
by XBOOLE_0:def 7;
( the Source of (AddNewEdge v1,v2) . the carrier' of G = v19 & the Target of (AddNewEdge v1,v2) . the carrier' of G = v29 )
by Th39;
then A11:
( vs9 . (len vs9) = <*v29,v19*> . 1 & <*v29,v19*> is_vertex_seq_of ep )
by Th16, FINSEQ_1:61;
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, Th9;
A14:
vs9 ^' <*v29,v19*> is_vertex_seq_of c9e
by A5, A11, GRAPH_2:47;
(vs9 ^' <*v29,v19*>) . 1 = vs . 1
by A3, GRAPH_2:14;
then
(vs9 ^' <*v29,v19*>) . 1 = (vs9 ^' <*v29,v19*>) . (len (vs9 ^' <*v29,v19*>))
by A6, FINSEQ_1:61;
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:44;
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:44
.=
((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 Th36;
reconsider dv9 = Degree v9,(rng c9e) as even Element of NAT by Th54;
A18:
Degree v9,(rng c9e) is even
by Th54;