let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ;
then vs . 1 in rng vs by FUNCT_1:def 3;
then A7: ( vs . 1 = x or vs . 1 = y ) by ;
A8: 1 <= len c by A1;
then A9: 1 in dom c by FINSEQ_3:25;
A10: vs /. (1 + 1) = vs . (1 + 1) by ;
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 ;
then vs . (1 + 1) in rng vs by FUNCT_1:def 3;
then ( vs . (1 + 1) = x or vs . (1 + 1) = y ) by ;
hence rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A1, A6, A5, A10, A11, A7, A9; :: thesis: verum