let G be non void Graph; :: thesis: for oc being non empty directed Chain of G st oc is cyclic holds
(vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)
let oc be non empty directed Chain of G; :: thesis: ( oc is cyclic implies (vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1) )
assume A1: oc is cyclic ; :: thesis: (vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)
set vsoc = vertex-seq oc;
A2: vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def 10;
thus (vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1) by A1, A2, Th5; :: thesis: verum