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))}
c <> {} by A1, Def8, CARD_1:47;
then G -VSet (rng c) = rng vs by A2, Th34;
then card (rng vs) = 2 by A1, Def8;
then consider x, y being set such that
A3: ( x <> y & rng vs = {x,y} ) by CARD_2:79;
set SG = the Source of G;
set TG = the Target of G;
set px = vs /. 1;
set px1 = vs /. (1 + 1);
A4: 1 <= len c by A1, Def8;
len vs = (len c) + 1 by A2, Def7;
then A5: ( 1 <= len vs & 1 <= 1 + 1 & 1 + 1 <= len vs ) by A4, NAT_1:12, XREAL_1:9;
then A6: ( vs /. 1 = vs . 1 & vs /. (1 + 1) = vs . (1 + 1) ) by FINSEQ_4:24;
c . 1 joins vs /. 1,vs /. (1 + 1) by A2, A4, Def7;
then A7: ( ( 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) ) ) by GRAPH_1:def 10;
( 1 in dom vs & 1 + 1 in dom vs ) by A5, FINSEQ_3:27;
then ( vs . 1 in rng vs & vs . (1 + 1) in rng vs ) by FUNCT_1:def 5;
then A8: ( ( vs . 1 = x or vs . 1 = y ) & ( vs . (1 + 1) = x or vs . (1 + 1) = y ) ) by A3, TARSKI:def 2;
1 in dom c by A4, FINSEQ_3:27;
hence rng vs = {(the Source of G . (c . 1)),(the Target of G . (c . 1))} by A1, A3, A6, A7, A8, Def8; :: thesis: verum