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: len (c1 ^ c2) = (len c1) + (len c2) by FINSEQ_1:22;
A2: vertex-seq c1 is_vertex_seq_of c1 by GRAPH_2:def 10;
then A3: ( vertex-seq c2 is_vertex_seq_of c2 & len (vertex-seq c1) = (len c1) + 1 ) by GRAPH_2:def 10;

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 A2, A3, GRAPH_2:43;
c1c2 is directed

proof

let n be Nat; :: according to GRAPH_1:def 15 :: thesis: ( not 1 <= n or len c1c2 <= n or the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) )
assume that
A5: 1 <= n and
A6: 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 A7: 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 + 1 in dom c1 by FINSEQ_3:25;
then A8: c1c2 . (n + 1) = c1 . (n + 1) by FINSEQ_1:def 7;
n in dom c1 by A5, A7, FINSEQ_3:25;
then 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, A7, A8, GRAPH_1:def 15; :: thesis: verum

end;

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

then n in dom c1 by FINSEQ_5:6;
then A10: c1c2 . n = c1 . n by FINSEQ_1:def 7;
1 in dom c2 by FINSEQ_5:6;
then A11: c1c2 . (n + 1) = c2 . 1 by A9, FINSEQ_1:def 7;
(vertex-seq c1) . ((len c1) + 1) = the Target of G . (c1 . (len c1)) by Th13;
hence the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A4, A9, A11, A10, GRAPH_2:def 10; :: thesis: verum

end;

suppose A12: 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:5;
A13: n = (len c1) + k ;
A14: n + 1 = (len c1) + (k + 1) ;
A15: k < len c2 by A1, A6, XREAL_1:19;
then ( 1 <= k + 1 & k + 1 <= len c2 ) by NAT_1:11, NAT_1:13;
then k + 1 in dom c2 by FINSEQ_3:25;
then A16: c1c2 . (n + 1) = c2 . (k + 1) by A14, FINSEQ_1:def 7;
n >= (len c1) + 1 by A12, NAT_1:13;
then A17: 1 <= k by XREAL_1:19;
then k in dom c2 by A15, FINSEQ_3:25;
then c1c2 . n = c2 . k by A13, FINSEQ_1:def 7;
hence the Source of G . (c1c2 . (n + 1)) = the Target of G . (c1c2 . n) by A17, A15, A16, GRAPH_1:def 15; :: thesis: verum

end;

end;

end;

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

end;

set n = len c1;
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 ;
A18: len c1 < len c1c2 by A1, XREAL_1:29;
A19: len c1 in dom c1 by FINSEQ_5:6;
then A20: c1c2 . (len c1) = c1 . (len c1) by FINSEQ_1:def 7;
1 <= len c1 by A19, FINSEQ_3:25;
then A21: the Source of G . (c1c2 . ((len c1) + 1)) = the Target of G . (c1c2 . (len c1)) by A18, GRAPH_1:def 15;
1 in dom c2 by FINSEQ_5:6;
then A22: c1c2 . ((len c1) + 1) = c2 . 1 by FINSEQ_1:def 7;
(vertex-seq c1) . ((len c1) + 1) = the Target of G . (c1 . (len c1)) by Th13;
hence (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 by A21, A22, A20, GRAPH_2:def 10; :: thesis: verum