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 that
A1: c is cyclic and
A2: vs is_vertex_seq_of c ; :: thesis: vs . 1 = vs . (len vs)
thus vs . 1 = vs . (len vs) by A1, A2, Lm1; :: thesis: verum