theorem Th13: :: MSSCYC_1:14

for G being non void Graph
for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))