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

A7: now

let n be Element of NAT ; :: thesis:
assume A8: ( 1 <= n & n <= len (vs1 ^' vs2) ) ; :: thesis:

per cases ;

suppose A9: n <= len vs1 ; :: thesis:

then A10: (vs1 ^' vs2) . n = vs1 . n by A8, Th14;
n in dom vs1 by A8, A9, FINSEQ_3:27;
hence (vs1 ^' vs2) . n in the carrier of G by A10, FINSEQ_2:13; :: thesis:

end;

suppose A11: n > len vs1 ; :: thesis:

then consider m being Nat such that
A12: n = (len vs1) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
m <> 0 by A11, A12;
then 0 < m ;
then A13: 0 + 1 <= m by NAT_1:13;
A14: 1 <= m + 1 by NAT_1:12;
(len vs1) + m <= (len vs1) + ((len vs2) - 1) by A5, A8, A12;
then m <= (len vs2) - 1 by XREAL_1:8;
then A15: m + 1 <= ((len vs2) - 1) + 1 by XREAL_1:8;
then m < len vs2 by NAT_1:13;
then A16: (vs1 ^' vs2) . ((len vs1) + m) = vs2 . (m + 1) by A13, Th15;
m + 1 in dom vs2 by A14, A15, FINSEQ_3:27;
hence (vs1 ^' vs2) . n in the carrier of G by A12, A16, FINSEQ_2:13; :: thesis:

end;

A17: now

let n be Element of NAT ; :: thesis:
assume ( 1 <= n & n <= len (c1 ^ c2) ) ; :: thesis:
then A18: n in dom (c1 ^ c2) by FINSEQ_3:27;

per cases by A18, FINSEQ_1:38;

suppose A19: n in dom c1 ; :: thesis:

then A20: (c1 ^ c2) . n = c1 . n by FINSEQ_1:def 7;
set v1 = vs1 /. n;
set v2 = vs1 /. (n + 1);
A21: ( 1 <= n & n <= len c1 ) by A19, FINSEQ_3:27;
then A22: c1 . n joins vs1 /. n,vs1 /. (n + 1) by A1, Def7;
A23: n <= len vs1 by A3, A21, NAT_1:12;
( 1 <= n + 1 & n + 1 <= (len c1) + 1 ) by A21, NAT_1:12, XREAL_1:8;
then A24: ( 1 <= n + 1 & n + 1 <= len vs1 ) by A1, Def7;
then A25: ( vs1 /. n = vs1 . n & vs1 /. (n + 1) = vs1 . (n + 1) ) by A21, A23, FINSEQ_4:24;
( (vs1 ^' vs2) . n = vs1 . n & (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) ) by A21, A23, A24, Th14;
hence ex v1, v2 being Element of the carrier of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n joins v1,v2 ) by A20, A22, A25; :: thesis:

end;

suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis:

then consider k being Nat such that
A26: ( k in dom c2 & n = (len c1) + k ) ;
A27: (c1 ^ c2) . n = c2 . k by A26, FINSEQ_1:def 7;
A28: ( 1 <= k & k <= len c2 ) by A26, FINSEQ_3:27;
then A29: ( 1 <= k + 1 & k <= len vs2 & k + 1 <= len vs2 ) by A3, NAT_1:12, XREAL_1:9;
reconsider k = k as Element of NAT by A26;
set v1 = vs2 /. k;
set v2 = vs2 /. (k + 1);
A30: ( vs2 /. k = vs2 . k & vs2 /. (k + 1) = vs2 . (k + 1) ) by A28, A29, FINSEQ_4:24;
A31: c2 . k joins vs2 /. k,vs2 /. (k + 1) by A2, A28, Def7;
A32: k <= len vs2 by A3, A28, NAT_1:12;
0 + 1 <= k by A26, FINSEQ_3:27;
then consider j being Element of NAT such that
A33: ( 0 <= j & j < len vs2 & k = j + 1 ) by A32, Th1;
A34: (vs1 ^' vs2) . n = vs2 . k

proof

per cases by A28, XXREAL_0:1;

suppose A35: 1 = k ; :: thesis:

0 + 1 <= len vs1 by A3, NAT_1:13;
hence (vs1 ^' vs2) . n = vs2 . k by A2, A3, A26, A35, Th14; :: thesis:

end;

suppose 1 < k ; :: thesis:

then A36: 1 <= j by A33, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . ((len vs1) + j) by A3, A26, A33
.= vs2 . k by A33, A36, Th15 ; :: thesis:

end;

A37: k < len vs2 by A3, A28, NAT_1:13;
(vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A26
.= vs2 . (k + 1) by A3, A28, A37, Th15 ;
hence ex v1, v2 being Element of the carrier of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n joins v1,v2 ) by A27, A30, A31, A34; :: thesis:

end;

thus c1 ^ c2 is Chain of G :: thesis:

proof

hereby :: according to GRAPH_1:def 12 :: thesis:

let n be Element of NAT ; :: thesis:
assume ( 1 <= n & n <= len (c1 ^ c2) ) ; :: thesis:
then A38: n in dom (c1 ^ c2) by FINSEQ_3:27;

per cases by A38, FINSEQ_1:38;

suppose A39: n in dom c1 ; :: thesis:

then A40: ( 1 <= n & n <= len c1 ) by FINSEQ_3:27;
(c1 ^ c2) . n = c1 . n by A39, FINSEQ_1:def 7;
hence (c1 ^ c2) . n in the carrier' of G by A40, GRAPH_1:def 12; :: thesis:

end;

suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis:

then consider k being Nat such that
A41: ( k in dom c2 & n = (len c1) + k ) ;
A42: (c1 ^ c2) . n = c2 . k by A41, FINSEQ_1:def 7;
( 1 <= k & k <= len c2 ) by A41, FINSEQ_3:27;
hence (c1 ^ c2) . n in the carrier' of G by A41, A42, GRAPH_1:def 12; :: thesis:

end;

thus ex b₁ being set st
( len b₁ = (len (c1 ^ c2)) + 1 & ( for b₂ being Element of NAT holds
( not 1 <= b₂ or not b₂ <= len b₁ or b₁ . b₂ in the carrier of G ) ) & ( for b₂ being Element of NAT holds
( not 1 <= b₂ or not b₂ <= len (c1 ^ c2) or ex b₃, b₄ being Element of the carrier of G st
( b₃ = b₁ . b₂ & b₄ = b₁ . (b₂ + 1) & (c1 ^ c2) . b₂ joins b₃,b₄ ) ) ) ) by A6, A7, A17; :: thesis:

end;