let G be Graph; :: thesis: for c being Chain of G
for vs being FinSequence of the carrier of G st c is cyclic & vs is_vertex_seq_of c holds
vs . 1 = vs . (len vs)
let c be Chain of G; :: thesis: for vs being FinSequence of the carrier of G st c is cyclic & vs is_vertex_seq_of c holds
vs . 1 = vs . (len vs)
let vs be FinSequence of the carrier of G; :: thesis: ( c is cyclic & vs is_vertex_seq_of c implies vs . 1 = vs . (len vs) )
assume A1: ( c is cyclic & vs is_vertex_seq_of c ) ; :: thesis: vs . 1 = vs . (len vs)

per cases ( c is empty or not c is empty ) ;

suppose A2: c is empty ; :: thesis: vs . 1 = vs . (len vs)

len vs = (len c) + 1 by A1, GRAPH_2:def 7
.= 0 + 1 by A2 ;
hence vs . 1 = vs . (len vs) ; :: thesis: verum

end;

suppose not c is empty ; :: thesis: vs . 1 = vs . (len vs)

thus vs . 1 = vs . (len vs) by A1, Lm1; :: thesis: verum

end;

end;