let G be non void Graph; :: thesis: for c1, c2 being non empty directed Chain of G holds
( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )
let c1, c2 be non empty directed Chain of G; :: thesis: ( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )
set vsc1 = vertex-seq c1;
set vsc2 = vertex-seq c2;
A1: ( vertex-seq c1 is_vertex_seq_of c1 & vertex-seq c2 is_vertex_seq_of c2 ) by GRAPH_2:def 11;
then A2: len (vertex-seq c1) = (len c1) + 1 by GRAPH_2:def 7;
A3: len (c1 ^ c2) = (len c1) + (len c2) by FINSEQ_1:35;

hereby :: thesis: ( c1 ^ c2 is non empty directed Chain of G implies (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 )

assume A4: (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 ; :: thesis: c1 ^ c2 is non empty directed Chain of G
then reconsider c1c2 = c1 ^ c2 as Chain of G by A1, A2, GRAPH_2:46;
c1c2 is directed

proof

let n be Element of NAT ; :: according to GRAPH_1:def 13 :: thesis: ( not 1 <= n or len c1c2 <= n or the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) )
assume A5: ( 1 <= n & n < len c1c2 ) ; :: thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)

per cases ( n < len c1 or n = len c1 or n > len c1 ) by XXREAL_0:1;

suppose A6: n < len c1 ; :: thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)

then ( 1 <= n + 1 & n + 1 <= len c1 ) by NAT_1:11, NAT_1:13;
then ( n in dom c1 & n + 1 in dom c1 ) by A5, A6, FINSEQ_3:27;
then ( c1c2 . (n + 1) = c1 . (n + 1) & c1c2 . n = c1 . n ) by FINSEQ_1:def 7;
hence the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A5, A6, GRAPH_1:def 13; :: thesis: verum

end;

suppose A7: n = len c1 ; :: thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)

A8: (vertex-seq c1) . ((len c1) + 1) = the Target of G . (c1 . (len c1)) by Th14;
( 1 in dom c2 & n in dom c1 ) by A7, FINSEQ_5:6;
then ( c1c2 . (n + 1) = c2 . 1 & c1c2 . n = c1 . n ) by A7, FINSEQ_1:def 7;
hence the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A4, A7, A8, GRAPH_2:def 11; :: thesis: verum

end;

suppose A9: n > len c1 ; :: thesis: the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n)

then reconsider k = n - (len c1) as Element of NAT by INT_1:18;
n >= (len c1) + 1 by A9, NAT_1:13;
then A10: 1 <= k by XREAL_1:21;
A11: k < len c2 by A3, A5, XREAL_1:21;
then ( 1 <= k + 1 & k + 1 <= len c2 ) by NAT_1:11, NAT_1:13;
then A12: ( k in dom c2 & k + 1 in dom c2 ) by A10, A11, FINSEQ_3:27;
A13: n = (len c1) + k ;
n + 1 = (len c1) + (k + 1) ;
then ( c1c2 . (n + 1) = c2 . (k + 1) & c1c2 . n = c2 . k ) by A12, A13, FINSEQ_1:def 7;
hence the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A10, A11, GRAPH_1:def 13; :: thesis: verum

end;

end;

end;

hence c1 ^ c2 is non empty directed Chain of G ; :: thesis: verum

end;

assume c1 ^ c2 is non empty directed Chain of G ; :: thesis: (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1
then reconsider c1c2 = c1 ^ c2 as non empty directed Chain of G ;
set n = len c1;
A14: (vertex-seq c1) . ((len c1) + 1) = the Target of G . (c1 . (len c1)) by Th14;
A15: len c1 in dom c1 by FINSEQ_5:6;
then A16: ( 1 <= len c1 & len c1 <= len c1 ) by FINSEQ_3:27;
len c1 < len c1c2 by A3, XREAL_1:31;
then A17: the Source of G . (c1c2 . ((len c1) + 1)) = the Target of G . (c1c2 . (len c1)) by A16, GRAPH_1:def 13;
1 in dom c2 by FINSEQ_5:6;
then ( c1c2 . ((len c1) + 1) = c2 . 1 & c1c2 . (len c1) = c1 . (len c1) ) by A15, FINSEQ_1:def 7;
hence (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 by A14, A17, GRAPH_2:def 11; :: thesis: verum