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 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; :: thesis: verum

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 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; :: thesis: verum