let G be non void Graph; :: thesis: for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))
let oc be non empty directed Chain of G; :: thesis: (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))
1 in dom oc by FINSEQ_5:6;
then 1 <= len oc by FINSEQ_3:25;
hence (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc)) by Th10; :: thesis: verum