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;

.= (len (c1 ^ c2)) + 1 by FINSEQ_1:22 ;

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

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

A16:
len vs1 = (len c1) + 1
by A1;(vs1 ^' vs2) . n in the carrier of G

let n be Nat; :: thesis: ( 1 <= n & n <= len (vs1 ^' vs2) implies (vs1 ^' vs2) . b_{1} in the carrier of G )

assume that

A7: 1 <= n and

A8: n <= len (vs1 ^' vs2) ; :: thesis: (vs1 ^' vs2) . b_{1} in the carrier of G

end;assume that

A7: 1 <= n and

A8: n <= len (vs1 ^' vs2) ; :: thesis: (vs1 ^' vs2) . b

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

end;

suppose A9:
n <= len vs1
; :: thesis: (vs1 ^' vs2) . b_{1} 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;(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

suppose A11:
n > len vs1
; :: thesis: (vs1 ^' vs2) . b_{1} 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;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

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 )

A48: len (vs1 ^' vs2) =
((len c1) + (len c2)) + 1
by A16, A4, A5
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_{3} = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b_{3} ) )

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_{3} = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b_{3} )

A20: n in dom (c1 ^ c2) by A18, A19, FINSEQ_3:25;

end;( v2 = (vs1 ^' vs2) . v1 & 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

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;

end;

( 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_{3} = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b_{3} )

( v2 = (vs1 ^' vs2) . v1 & 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;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

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_{3} = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b_{3} )

( k in dom c2 & n = (len c1) + k ) ; :: thesis: ex v1, v2 being Element of G st

( v2 = (vs1 ^' vs2) . v1 & 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

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;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
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

.= (len (c1 ^ c2)) + 1 by FINSEQ_1:22 ;

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

proof
_{1} being set st

( len b_{1} = (len (c1 ^ c2)) + 1 & ( for b_{2} being set holds

( not 1 <= b_{2} or not b_{2} <= len b_{1} or b_{1} . b_{2} in the carrier of G ) ) & ( for b_{2} being set holds

( not 1 <= b_{2} or not b_{2} <= len (c1 ^ c2) or ex b_{3}, b_{4} being Element of the carrier of G st

( b_{3} = b_{1} . b_{2} & b_{4} = b_{1} . (b_{2} + 1) & (c1 ^ c2) . b_{2} joins b_{3},b_{4} ) ) ) )
by A48, A6, A17; :: thesis: verum

end;

hereby :: according to GRAPH_1:def 14 :: thesis: ex b_{1} being set st

( len b_{1} = (len (c1 ^ c2)) + 1 & ( for b_{2} being set holds

( not 1 <= b_{2} or not b_{2} <= len b_{1} or b_{1} . b_{2} in the carrier of G ) ) & ( for b_{2} being set holds

( not 1 <= b_{2} or not b_{2} <= len (c1 ^ c2) or ex b_{3}, b_{4} being Element of the carrier of G st

( b_{3} = b_{1} . b_{2} & b_{4} = b_{1} . (b_{2} + 1) & (c1 ^ c2) . b_{2} joins b_{3},b_{4} ) ) ) )

thus
ex b( len b

( not 1 <= b

( not 1 <= b

( b

let n be Nat; :: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b_{1} in the carrier' of G )

assume that

A49: 1 <= n and

A50: n <= len (c1 ^ c2) ; :: thesis: (c1 ^ c2) . b_{1} in the carrier' of G

A51: n in dom (c1 ^ c2) by A49, A50, FINSEQ_3:25;

end;assume that

A49: 1 <= n and

A50: n <= len (c1 ^ c2) ; :: thesis: (c1 ^ c2) . b

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;

end;

( k in dom c2 & n = (len c1) + k ) ) by A51, FINSEQ_1:25;

suppose A52:
n in dom c1
; :: thesis: (c1 ^ c2) . b_{1} 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;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

suppose
ex k being Nat st

( k in dom c2 & n = (len c1) + k ) ; :: thesis: (c1 ^ c2) . b_{1} in the carrier' of G

( k in dom c2 & n = (len c1) + k ) ; :: thesis: (c1 ^ c2) . b

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;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

( len b

( not 1 <= b

( not 1 <= b

( b