let G be non void Graph; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( (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; :: thesis: verum