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 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 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 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 ; ( 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 G' = AddNewEdge v1,v2;
reconsider vs' = vs as FinSequence of the carrier of (AddNewEdge v1,v2) by Def7;
reconsider c' = c as Path of by Th42;
A5:
vs' is_vertex_seq_of c'
by A2, Th41;
reconsider v' = v, v1' = v1, v2' = v2 as Vertex of (AddNewEdge v1,v2) by Def7;
set v21' = <*v2',v1'*>;
set vs'e = vs' ^' <*v2',v1'*>;
len <*v2',v1'*> = 2
by FINSEQ_1:61;
then A6:
(vs' ^' <*v2',v1'*>) . (len (vs' ^' <*v2',v1'*>)) = <*v2',v1'*> . 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 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 = v1' & the Target of (AddNewEdge v1,v2) . the carrier' of G = v2' )
by Th39;
then A11:
( vs' . (len vs') = <*v2',v1'*> . 1 & <*v2',v1'*> 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 c' misses rng ep
then reconsider c'e = c' ^ ep as Path of by A5, A11, Th9;
A14:
vs' ^' <*v2',v1'*> is_vertex_seq_of c'e
by A5, A11, GRAPH_2:47;
(vs' ^' <*v2',v1'*>) . 1 = vs . 1
by A3, GRAPH_2:14;
then
(vs' ^' <*v2',v1'*>) . 1 = (vs' ^' <*v2',v1'*>) . (len (vs' ^' <*v2',v1'*>))
by A6, FINSEQ_1:61;
then reconsider c'e = c'e as cyclic Path of cyclic by A14, MSSCYC_1:def 2;
rng c'e = (rng c) \/ (rng ep)
by FINSEQ_1:44;
then A15:
the carrier' of G in rng c'e
by A7, A8, XBOOLE_0:def 3;
A16: (rng c'e) /\ 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 c'e) = Degree v,(rng c)
by Th36;
reconsider dv' = Degree v',(rng c'e) as even Element of NAT by Th54;
A18:
Degree v',(rng c'e) is even
by Th54;