let G be Graph; :: thesis: for vs1, vs2, vs being FinSequence of the carrier of G
for c1, c2, c being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_vertex_seq_of c
let vs1, vs2, vs be FinSequence of the carrier of G; :: thesis: for c1, c2, c being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_vertex_seq_of c
let c1, c2, c be Chain of G; :: thesis: ( vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 implies vs is_vertex_seq_of c )
assume that
A1: vs1 is_vertex_seq_of c1 and
A2: ( vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 ) ; :: thesis: ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_vertex_seq_of c )
assume that
A3: c = c1 ^ c2 and
A4: vs = vs1 ^' vs2 ; :: thesis: vs is_vertex_seq_of c
A5: ( len vs1 = (len c1) + 1 & len vs2 = (len c2) + 1 ) by A1, A2, Def7;
then A6: ( vs1 <> {} & vs2 <> {} ) ;
set q = c1 ^ c2;
set p = vs1 ^' vs2;
(len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by A6, Th13;
then A7: len (vs1 ^' vs2) = ((len c1) + (len c2)) + 1 by A5
.= (len (c1 ^ c2)) + 1 by FINSEQ_1:35 ;
reconsider p = vs1 ^' vs2 as FinSequence of the carrier of G ;

now

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b₁ joins p /. b₁,p /. (b₁ + 1) )
assume that
A8: 1 <= n and
A9: n <= len (c1 ^ c2) ; :: thesis: (c1 ^ c2) . b₁ joins p /. b₁,p /. (b₁ + 1)
( n <= len p & 1 <= n + 1 & n + 1 <= len p ) by A7, A9, NAT_1:12, XREAL_1:9;
then A10: ( p /. n = p . n & p /. (n + 1) = p . (n + 1) ) by A8, FINSEQ_4:24;
A11: n in dom (c1 ^ c2) by A8, A9, FINSEQ_3:27;

per cases ( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ) by A11, FINSEQ_1:38;

suppose A12: n in dom c1 ; :: thesis: (c1 ^ c2) . b₁ joins p /. b₁,p /. (b₁ + 1)

set v1 = vs1 /. n;
set v2 = vs1 /. (n + 1);
A13: ( 1 <= n & n <= len c1 ) by A12, FINSEQ_3:27;
then A14: c1 . n joins vs1 /. n,vs1 /. (n + 1) by A1, Def7;
A15: n <= len vs1 by A5, A13, NAT_1:12;
( 1 <= n + 1 & n + 1 <= (len c1) + 1 ) by A13, NAT_1:12, XREAL_1:8;
then A16: ( 1 <= n + 1 & n + 1 <= len vs1 ) by A1, Def7;
then A17: ( vs1 /. n = vs1 . n & vs1 /. (n + 1) = vs1 . (n + 1) ) by A13, A15, FINSEQ_4:24;
( p . n = vs1 . n & p . (n + 1) = vs1 . (n + 1) ) by A13, A15, A16, Th14;
hence (c1 ^ c2) . n joins p /. n,p /. (n + 1) by A10, A12, A14, A17, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis: (c1 ^ c2) . b₁ joins p /. b₁,p /. (b₁ + 1)

then consider k being Element of NAT such that
A18: ( k in dom c2 & n = (len c1) + k ) ;
A19: ( 1 <= k & k <= len c2 ) by A18, FINSEQ_3:27;
then A20: ( 1 <= k + 1 & k <= len vs2 & k + 1 <= len vs2 ) by A5, NAT_1:12, XREAL_1:9;
set v1 = vs2 /. k;
set v2 = vs2 /. (k + 1);
A21: ( vs2 /. k = vs2 . k & vs2 /. (k + 1) = vs2 . (k + 1) ) by A19, A20, FINSEQ_4:24;
A22: c2 . k joins vs2 /. k,vs2 /. (k + 1) by A2, A19, Def7;
A23: k <= len vs2 by A5, A19, NAT_1:12;
0 + 1 <= k by A18, FINSEQ_3:27;
then consider j being Element of NAT such that
A24: ( 0 <= j & j < len vs2 & k = j + 1 ) by A23, Th1;
A25: p . n = vs2 . k

proof

per cases ( 1 = k or 1 < k ) by A19, XXREAL_0:1;

suppose A26: 1 = k ; :: thesis: p . n = vs2 . k

0 + 1 <= len vs1 by A5, NAT_1:13;
hence p . n = vs2 . k by A2, A5, A18, A26, Th14; :: thesis: verum

end;

suppose 1 < k ; :: thesis: p . n = vs2 . k

then A27: 1 <= j by A24, NAT_1:13;
thus p . n = p . ((len vs1) + j) by A5, A18, A24
.= vs2 . k by A24, A27, Th15 ; :: thesis: verum

end;

end;

end;

A28: k < len vs2 by A5, A19, NAT_1:13;
p . (n + 1) = p . (((len c1) + 1) + k) by A18
.= vs2 . (k + 1) by A5, A19, A28, Th15 ;
hence (c1 ^ c2) . n joins p /. n,p /. (n + 1) by A10, A18, A21, A22, A25, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence vs is_vertex_seq_of c by A3, A4, A7, Def7; :: thesis: verum