let G be finite Graph; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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
; :: thesis: ( Degree v,(rng c) is even iff ( v <> vs . 1 & v <> vs . (len vs) ) )
set E = the carrier' of G;
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 v' = v, v1' = v1, v2' = v2 as Vertex of (AddNewEdge v1,v2) by Def7;
reconsider c' = c as Path of AddNewEdge v1,v2 by Th42;
reconsider vs' = vs as FinSequence of the carrier of (AddNewEdge v1,v2) by Def7;
set e = the carrier' of G;
A5:
the carrier' of (AddNewEdge v1,v2) = the carrier' of G \/ {the carrier' of G}
by Def7;
A6:
not the carrier' of G in the carrier' of G
;
A7:
the carrier' of G in {the carrier' of G}
by TARSKI:def 1;
then
the carrier' of G in the carrier' of (AddNewEdge v1,v2)
by A5, XBOOLE_0:def 3;
then reconsider ep = <*the carrier' of G*> as Path of AddNewEdge v1,v2 by Th7;
set v21' = <*v2',v1'*>;
set vs'e = vs' ^' <*v2',v1'*>;
A8:
rng c c= the carrier' of G
by FINSEQ_1:def 4;
then A9:
not the carrier' of G in rng c
by A6;
A10:
rng ep = {the carrier' of G}
by FINSEQ_1:56;
A11:
rng c' misses rng ep
A13:
vs' is_vertex_seq_of c'
by A2, Th41;
A14:
vs' . (len vs') = <*v2',v1'*> . 1
by FINSEQ_1:61;
( 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 A15:
<*v2',v1'*> is_vertex_seq_of ep
by Th16;
A16:
(vs' ^' <*v2',v1'*>) . 1 = vs . 1
by A3, GRAPH_2:14;
len <*v2',v1'*> = 2
by FINSEQ_1:61;
then
(vs' ^' <*v2',v1'*>) . (len (vs' ^' <*v2',v1'*>)) = <*v2',v1'*> . 2
by GRAPH_2:16;
then A17:
(vs' ^' <*v2',v1'*>) . 1 = (vs' ^' <*v2',v1'*>) . (len (vs' ^' <*v2',v1'*>))
by A16, FINSEQ_1:61;
reconsider c'e = c' ^ ep as Path of AddNewEdge v1,v2 by A11, A13, A14, A15, Th9;
vs' ^' <*v2',v1'*> is_vertex_seq_of c'e
by A13, A14, A15, GRAPH_2:47;
then reconsider c'e = c'e as cyclic Path of AddNewEdge v1,v2 by A17, MSSCYC_1:def 2;
A18:
Degree v',(rng c'e) is even
by Th54;
reconsider dv' = Degree v',(rng c'e) as even Element of NAT by Th54;
rng ep misses the carrier' of G
by A6, A10, ZFMISC_1:56;
then A19:
(rng ep) /\ the carrier' of G = {}
by XBOOLE_0:def 7;
A20: (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 A19, XBOOLE_1:23
.=
rng c
by A8, XBOOLE_1:28
;
then A21:
Degree v,(rng c'e) = Degree v,(rng c)
by Th36;
rng c'e = (rng c) \/ (rng ep)
by FINSEQ_1:44;
then A22:
the carrier' of G in rng c'e
by A7, A10, XBOOLE_0:def 3;