let G be Graph; :: thesis: for c being Chain of G
for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
let c be Chain of G; :: thesis: for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
let p be FinSequence of the carrier of G; :: thesis: ( c is cyclic & p is_vertex_seq_of c implies p . 1 = p . (len p) )
assume that
A1: c is cyclic and
A2: p is_vertex_seq_of c ; :: thesis: p . 1 = p . (len p)
consider P being FinSequence of the carrier of G such that
A3: P is_vertex_seq_of c and
A4: P . 1 = P . (len P) by A1;

per cases ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) or ( not card the carrier of G = 1 & not ( c <> {} & not c alternates_vertices_in G ) ) ) ;

suppose ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ; :: thesis: p . 1 = p . (len p)

then ( P = vertex-seq c & p = vertex-seq c ) by A2, A3, GRAPH_2:def 8;
hence p . 1 = p . (len p) by A4; :: thesis: verum

end;

suppose A5: ( not card the carrier of G = 1 & not ( c <> {} & not c alternates_vertices_in G ) ) ; :: thesis: p . 1 = p . (len p)

A6: len p = (len c) + 1 by A2;
A7: len P = (len c) + 1 by A3;

now :: thesis: p . 1 = p . (len p)

per cases ( ( card the carrier of G <> 1 & c = {} ) or ( card the carrier of G <> 1 & c alternates_vertices_in G ) ) by A5;

suppose ( card the carrier of G <> 1 & c = {} ) ; :: thesis: p . 1 = p . (len p)

then len c = 0 ;
hence p . 1 = p . (len p) by A6; :: thesis: verum

end;

suppose A8: ( card the carrier of G <> 1 & c alternates_vertices_in G ) ; :: thesis: p . 1 = p . (len p)

then A9: ( p is TwoValued & p is Alternating & P is TwoValued & P is Alternating ) by A2, A3, GRAPH_2:37;

now :: thesis: ( p <> P implies p . 1 = p . (len p) )

set S = the Source of G;
set T = the Target of G;
assume p <> P ; :: thesis: p . 1 = p . (len p)
A10: rng p = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A2, A8, GRAPH_2:36;
A11: 1 <= len p by A6, NAT_1:11;
then len p in dom p by FINSEQ_3:25;
then p . (len p) in rng p by FUNCT_1:def 3;
then A12: ( p . (len p) = the Source of G . (c . 1) or p . (len p) = the Target of G . (c . 1) ) by A10, TARSKI:def 2;
A13: rng P = {( the Source of G . (c . 1)),( the Target of G . (c . 1))} by A3, A8, GRAPH_2:36;
1 in dom P by A6, A7, A11, FINSEQ_3:25;
then P . 1 in rng p by A10, A13, FUNCT_1:def 3;
then A14: ( P . 1 = the Source of G . (c . 1) or P . 1 = the Target of G . (c . 1) ) by A10, TARSKI:def 2;
1 in dom p by A11, FINSEQ_3:25;
then p . 1 in rng p by FUNCT_1:def 3;
then ( p . 1 = the Source of G . (c . 1) or p . 1 = the Target of G . (c . 1) ) by A10, TARSKI:def 2;
hence p . 1 = p . (len p) by A4, A6, A7, A9, A10, A13, A11, A12, A14, FINSEQ_6:147; :: thesis: verum

end;

hence p . 1 = p . (len p) by A4; :: thesis: verum

end;

end;

end;

hence p . 1 = p . (len p) ; :: thesis: verum

end;

end;