let G be Graph; for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
let vs be FinSequence of the carrier of G; for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
let c be Chain of G; ( c alternates_vertices_in G & vs is_vertex_seq_of c implies rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} )
assume that
A1:
c alternates_vertices_in G
and
A2:
vs is_vertex_seq_of c
; rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
set px1 = vs /. (1 + 1);
set TG = the Target of G;
set SG = the Source of G;
set px = vs /. 1;
A3:
len vs = (len c) + 1
by A2;
then A4:
1 <= len vs
by NAT_1:12;
then A5:
vs /. 1 = vs . 1
by FINSEQ_4:15;
c <> {}
by A1;
then
card (rng vs) = 2
by A1, A2, Th31;
then consider x, y being object such that
x <> y
and
A6:
rng vs = {x,y}
by CARD_2:60;
1 in dom vs
by A4, FINSEQ_3:25;
then
vs . 1 in rng vs
by FUNCT_1:def 3;
then A7:
( vs . 1 = x or vs . 1 = y )
by A6, TARSKI:def 2;
A8:
1 <= len c
by A1;
then A9:
1 in dom c
by FINSEQ_3:25;
A10:
vs /. (1 + 1) = vs . (1 + 1)
by A8, A3, FINSEQ_4:15, XREAL_1:7;
c . 1 joins vs /. 1,vs /. (1 + 1)
by A2, A8;
then A11:
( ( the Target of G . (c . 1) = vs /. (1 + 1) & the Source of G . (c . 1) = vs /. 1 ) or ( the Target of G . (c . 1) = vs /. 1 & the Source of G . (c . 1) = vs /. (1 + 1) ) )
;
1 + 1 in dom vs
by FINSEQ_3:25, A8, A3, XREAL_1:7;
then
vs . (1 + 1) in rng vs
by FUNCT_1:def 3;
then
( vs . (1 + 1) = x or vs . (1 + 1) = y )
by A6, TARSKI:def 2;
hence
rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}
by A1, A6, A5, A10, A11, A7, A9; verum