let G be non empty 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 A1: ( c is cyclic & p is_vertex_seq_of c ) ; :: thesis: p . 1 = p . (len p)
then consider P being FinSequence of the carrier of G such that
A2: ( P is_vertex_seq_of c & P . 1 = P . (len P) ) by Def2;

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 A1, A2, GRAPH_2:def 9;
hence p . 1 = p . (len p) by A2; :: thesis: verum

end;

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

A4: ( len p = (len c) + 1 & len P = (len c) + 1 ) by A1, A2, GRAPH_2:def 7;

now

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

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

end;

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

then A6: ( p is TwoValued & p is Alternating & P is TwoValued & P is Alternating ) by A1, A2, GRAPH_2:40;

now

assume p <> P ; :: thesis: p . 1 = p . (len p)
set S = the Source of G;
set T = the Target of G;
A7: ( rng p = {(the Source of G . (c . 1)),(the Target of G . (c . 1))} & rng P = {(the Source of G . (c . 1)),(the Target of G . (c . 1))} ) by A1, A2, A5, GRAPH_2:39;
A8: 1 <= len p by A4, NAT_1:11;
then ( 1 in dom p & len p in dom p & 1 in dom P & len p in dom P ) by A4, FINSEQ_3:27;
then ( p . 1 in rng p & P . 1 in rng p & p . (len p) in rng p & P . (len p) in rng p ) by A7, FUNCT_1:def 5;
then ( ( p . 1 = the Source of G . (c . 1) or p . 1 = the Target of G . (c . 1) ) & ( p . (len p) = the Source of G . (c . 1) or p . (len p) = the Target of G . (c . 1) ) & ( P . 1 = the Source of G . (c . 1) or P . 1 = the Target of G . (c . 1) ) & ( P . (len p) = the Source of G . (c . 1) or P . (len p) = the Target of G . (c . 1) ) ) by A7, TARSKI:def 2;
hence p . 1 = p . (len p) by A2, A4, A6, A7, A8, GRAPH_2:21; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;