let G be Graph; :: thesis: for vs1, vs2 being FinSequence of the carrier of G
for c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds
c1 ^ c2 is Chain of G
let vs1, vs2 be FinSequence of the carrier of G; :: thesis: for c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds
c1 ^ c2 is Chain of G
let c1, c2 be Chain of G; :: thesis: ( vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 implies c1 ^ c2 is Chain of G )
assume that
A1: vs1 is_vertex_seq_of c1 and
A2: vs2 is_vertex_seq_of c2 and
A3: vs1 . (len vs1) = vs2 . 1 ; :: thesis: c1 ^ c2 is Chain of G
set q = c1 ^ c2;
set p = vs1 ^' vs2;
A4: len vs2 = (len c2) + 1 by A2;
then vs2 <> {} ;
then A5: (len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by FINSEQ_6:139;

A6: now :: thesis: for n being Nat st 1 <= n & n <= len (vs1 ^' vs2) holds
(vs1 ^' vs2) . n in the carrier of G

let n be Nat; :: thesis: ( 1 <= n & n <= len (vs1 ^' vs2) implies (vs1 ^' vs2) . b₁ in the carrier of G )
assume that
A7: 1 <= n and
A8: n <= len (vs1 ^' vs2) ; :: thesis: (vs1 ^' vs2) . b₁ in the carrier of G

per cases ( n <= len vs1 or n > len vs1 ) ;

suppose A9: n <= len vs1 ; :: thesis: (vs1 ^' vs2) . b₁ in the carrier of G

then A10: n in dom vs1 by A7, FINSEQ_3:25;
(vs1 ^' vs2) . n = vs1 . n by A7, A9, FINSEQ_6:140;
hence (vs1 ^' vs2) . n in the carrier of G by A10, FINSEQ_2:11; :: thesis: verum

end;

suppose A11: n > len vs1 ; :: thesis: (vs1 ^' vs2) . b₁ in the carrier of G

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 12;
m <> 0 by A11, A12;
then A13: 0 + 1 <= m by NAT_1:13;
(len vs1) + m <= (len vs1) + ((len vs2) - 1) by A5, A8, A12;
then m <= (len vs2) - 1 by XREAL_1:6;
then A14: m + 1 <= ((len vs2) - 1) + 1 by XREAL_1:6;
1 <= m + 1 by NAT_1:12;
then A15: m + 1 in dom vs2 by A14, FINSEQ_3:25;
m < len vs2 by A14, NAT_1:13;
then (vs1 ^' vs2) . ((len vs1) + m) = vs2 . (m + 1) by A13, FINSEQ_6:141;
hence (vs1 ^' vs2) . n in the carrier of G by A12, A15, FINSEQ_2:11; :: thesis: verum

end;

end;

end;

A16: len vs1 = (len c1) + 1 by A1;

A17: now :: thesis: for n being Nat st 1 <= n & n <= len (c1 ^ c2) holds
ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n joins v1,v2 )

let n be Nat; :: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b₃ = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b₃ ) )
assume that
A18: 1 <= n and
A19: n <= len (c1 ^ c2) ; :: thesis: ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b₃ = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b₃ )
A20: n in dom (c1 ^ c2) by A18, A19, FINSEQ_3:25;

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

suppose A21: n in dom c1 ; :: thesis: ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b₃ = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b₃ )

set v2 = vs1 /. (n + 1);
set v1 = vs1 /. n;
A22: (c1 ^ c2) . n = c1 . n by A21, FINSEQ_1:def 7;
A23: 1 <= n by A21, FINSEQ_3:25;
A24: n <= len c1 by A21, FINSEQ_3:25;
then A25: n + 1 <= len vs1 by A1, XREAL_1:6;
then A26: vs1 /. (n + 1) = vs1 . (n + 1) by FINSEQ_4:15, NAT_1:12;
A27: n <= len vs1 by A16, A24, NAT_1:12;
then A28: vs1 /. n = vs1 . n by A23, FINSEQ_4:15;
A29: (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) by A25, FINSEQ_6:140, NAT_1:12;
A30: (vs1 ^' vs2) . n = vs1 . n by A23, A27, FINSEQ_6:140;
c1 . n joins vs1 /. n,vs1 /. (n + 1) by A1, A23, A24;
hence ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n joins v1,v2 ) by A22, A28, A26, A30, A29; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis: ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b₃ = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b₃ )

then consider k being Nat such that
A31: k in dom c2 and
A32: n = (len c1) + k ;
A33: (c1 ^ c2) . n = c2 . k by A31, A32, FINSEQ_1:def 7;
A34: 1 <= k + 1 by NAT_1:12;
A35: 1 <= k by A31, FINSEQ_3:25;
A36: k <= len c2 by A31, FINSEQ_3:25;
then A37: k <= len vs2 by A4, NAT_1:12;
reconsider k = k as Element of NAT by A31;
A38: 0 + 1 <= k by A31, FINSEQ_3:25;
A39: vs2 /. (k + 1) = vs2 . (k + 1) by A4, A36, A34, FINSEQ_4:15, XREAL_1:7;
A40: k < len vs2 by A4, A36, NAT_1:13;
k <= len vs2 by A4, A36, NAT_1:12;
then consider j being Nat such that
0 <= j and
A41: j < len vs2 and
A42: k = j + 1 by A38, FINSEQ_6:127;
A43: (vs1 ^' vs2) . n = vs2 . k

proof

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

suppose A44: 1 = k ; :: thesis: (vs1 ^' vs2) . n = vs2 . k

0 + 1 <= len vs1 by A16, NAT_1:13;
hence (vs1 ^' vs2) . n = vs2 . k by A3, A16, A32, A44, FINSEQ_6:140; :: thesis: verum

end;

suppose 1 < k ; :: thesis: (vs1 ^' vs2) . n = vs2 . k

then A45: 1 <= j by A42, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . ((len vs1) + j) by A16, A32, A42
.= vs2 . k by A41, A42, A45, FINSEQ_6:141 ; :: thesis: verum

end;

end;

end;

set v2 = vs2 /. (k + 1);
set v1 = vs2 /. k;
A46: c2 . k joins vs2 /. k,vs2 /. (k + 1) by A2, A35, A36;
A47: vs2 /. k = vs2 . k by A35, A37, FINSEQ_4:15;
(vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A32
.= vs2 . (k + 1) by A16, A35, A40, FINSEQ_6:141 ;
hence ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n joins v1,v2 ) by A33, A47, A39, A46, A43; :: thesis: verum

end;

end;

end;

A48: len (vs1 ^' vs2) = ((len c1) + (len c2)) + 1 by A16, A4, A5
.= (len (c1 ^ c2)) + 1 by FINSEQ_1:22 ;
thus c1 ^ c2 is Chain of G :: thesis: verum

proof

hereby :: according to GRAPH_1:def 14 :: thesis: ex b₁ being set st
( len b₁ = (len (c1 ^ c2)) + 1 & ( for b₂ being set holds
( not 1 <= b₂ or not b₂ <= len b₁ or b₁ . b₂ in the carrier of G ) ) & ( for b₂ being set 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₄ ) ) ) )

let n be Nat; :: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b₁ in the carrier' of G )
assume that
A49: 1 <= n and
A50: n <= len (c1 ^ c2) ; :: thesis: (c1 ^ c2) . b₁ in the carrier' of G
A51: n in dom (c1 ^ c2) by A49, A50, FINSEQ_3:25;

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

suppose A52: n in dom c1 ; :: thesis: (c1 ^ c2) . b₁ in the carrier' of G

then A53: (c1 ^ c2) . n = c1 . n by FINSEQ_1:def 7;
A54: n <= len c1 by A52, FINSEQ_3:25;
1 <= n by A52, FINSEQ_3:25;
hence (c1 ^ c2) . n in the carrier' of G by A54, A53, GRAPH_1:def 14; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis: (c1 ^ c2) . b₁ in the carrier' of G

then consider k being Nat such that
A55: k in dom c2 and
A56: n = (len c1) + k ;
A57: 1 <= k by A55, FINSEQ_3:25;
A58: k <= len c2 by A55, FINSEQ_3:25;
(c1 ^ c2) . n = c2 . k by A55, A56, FINSEQ_1:def 7;
hence (c1 ^ c2) . n in the carrier' of G by A57, A58, GRAPH_1:def 14; :: thesis: verum

end;

end;

end;

thus ex b₁ being set st
( len b₁ = (len (c1 ^ c2)) + 1 & ( for b₂ being set holds
( not 1 <= b₂ or not b₂ <= len b₁ or b₁ . b₂ in the carrier of G ) ) & ( for b₂ being set 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 A48, A6, A17; :: thesis: verum

end;