let G be non void Graph; for c, c1, c2 being non empty directed Chain of G st c = c1 ^ c2 holds
( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
let c, c1, c2 be non empty directed Chain of G; ( c = c1 ^ c2 implies ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) ) )
1 in dom c
by FINSEQ_5:6;
then
1 <= len c
by FINSEQ_3:25;
then A1:
( (vertex-seq c) . 1 = the Source of G . (c . 1) & (vertex-seq c) . ((len c) + 1) = the Target of G . (c . (len c)) )
by Th10;
A2:
1 in dom c1
by FINSEQ_5:6;
then
1 <= len c1
by FINSEQ_3:25;
then A3:
(vertex-seq c1) . 1 = the Source of G . (c1 . 1)
by Th10;
1 in dom c2
by FINSEQ_5:6;
then
1 <= len c2
by FINSEQ_3:25;
then A4:
(vertex-seq c2) . ((len c2) + 1) = the Target of G . (c2 . (len c2))
by Th10;
assume A5:
c = c1 ^ c2
; ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
then
( len c2 in dom c2 & len c = (len c1) + (len c2) )
by FINSEQ_1:22, FINSEQ_5:6;
hence
( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
by A5, A2, A3, A1, A4, FINSEQ_1:def 7; verum