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) ) )
assume A1: c = c1 ^ c2 ; :: thesis: ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
A2: ( 1 in dom c & 1 in dom c1 & 1 in dom c2 & len c2 in dom c2 ) by FINSEQ_5:6;
A3: len c = (len c1) + (len c2) by A1, FINSEQ_1:35;
( 1 <= len c & 1 <= len c1 & 1 <= len c2 ) by A2, FINSEQ_3:27;
then ( (vertex-seq c) . 1 = the Source of G . (c . 1) & (vertex-seq c1) . 1 = the Source of G . (c1 . 1) & (vertex-seq c) . ((len c) + 1) = the Target of G . (c . (len c)) & (vertex-seq c2) . ((len c2) + 1) = the Target of G . (c2 . (len c2)) ) by Th11;
hence ( (vertex-seq c) . 1 = (vertex-seq c1) . 1 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) ) by A1, A2, A3, FINSEQ_1:def 7; :: thesis: verum