let G be Graph; :: thesis: for vs, vs1, vs2 being FinSequence of the carrier of G

for c, c1, c2 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 vs, vs1, vs2 be FinSequence of the carrier of G; :: thesis: for c, c1, c2 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 c, c1, c2 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 and

A3: vs1 . (len vs1) = vs2 . 1 ; :: thesis: ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_vertex_seq_of c )

set p = vs1 ^' vs2;

set q = c1 ^ c2;

assume that

A4: c = c1 ^ c2 and

A5: vs = vs1 ^' vs2 ; :: thesis: vs is_vertex_seq_of c

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

A7: len vs2 = (len c2) + 1 by A2;

then vs2 <> {} ;

then (len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by FINSEQ_6:139;

then A8: len (vs1 ^' vs2) = ((len c1) + (len c2)) + 1 by A6, A7

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

reconsider p = vs1 ^' vs2 as FinSequence of the carrier of G ;

for c, c1, c2 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 vs, vs1, vs2 be FinSequence of the carrier of G; :: thesis: for c, c1, c2 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 c, c1, c2 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 and

A3: vs1 . (len vs1) = vs2 . 1 ; :: thesis: ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_vertex_seq_of c )

set p = vs1 ^' vs2;

set q = c1 ^ c2;

assume that

A4: c = c1 ^ c2 and

A5: vs = vs1 ^' vs2 ; :: thesis: vs is_vertex_seq_of c

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

A7: len vs2 = (len c2) + 1 by A2;

then vs2 <> {} ;

then (len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by FINSEQ_6:139;

then A8: len (vs1 ^' vs2) = ((len c1) + (len c2)) + 1 by A6, A7

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

reconsider p = vs1 ^' vs2 as FinSequence of the carrier of G ;

now :: thesis: for n being Nat st 1 <= n & n <= len (c1 ^ c2) holds

(c1 ^ c2) . n joins p /. n,p /. (n + 1)

hence
vs is_vertex_seq_of c
by A4, A5, A8; :: thesis: verum(c1 ^ c2) . n joins p /. n,p /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b_{1} joins p /. b_{1},p /. (b_{1} + 1) )

assume that

A9: 1 <= n and

A10: n <= len (c1 ^ c2) ; :: thesis: (c1 ^ c2) . b_{1} joins p /. b_{1},p /. (b_{1} + 1)

A11: n in dom (c1 ^ c2) by A9, A10, FINSEQ_3:25;

n <= len p by A8, A10, NAT_1:12;

then A12: p /. n = p . n by A9, FINSEQ_4:15;

1 <= n + 1 by NAT_1:12;

then A13: p /. (n + 1) = p . (n + 1) by A8, A10, FINSEQ_4:15, XREAL_1:7;

end;assume that

A9: 1 <= n and

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

A11: n in dom (c1 ^ c2) by A9, A10, FINSEQ_3:25;

n <= len p by A8, A10, NAT_1:12;

then A12: p /. n = p . n by A9, FINSEQ_4:15;

1 <= n + 1 by NAT_1:12;

then A13: p /. (n + 1) = p . (n + 1) by A8, A10, FINSEQ_4:15, XREAL_1:7;

per cases
( n in dom c1 or ex k being Nat st

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

end;

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

suppose A14:
n in dom c1
; :: thesis: (c1 ^ c2) . b_{1} joins p /. b_{1},p /. (b_{1} + 1)

set v2 = vs1 /. (n + 1);

set v1 = vs1 /. n;

A15: 1 <= n by A14, FINSEQ_3:25;

A16: n <= len c1 by A14, FINSEQ_3:25;

then A17: n + 1 <= len vs1 by A1, XREAL_1:6;

then A18: vs1 /. (n + 1) = vs1 . (n + 1) by FINSEQ_4:15, NAT_1:12;

A19: n <= len vs1 by A6, A16, NAT_1:12;

then A20: vs1 /. n = vs1 . n by A15, FINSEQ_4:15;

A21: p . (n + 1) = vs1 . (n + 1) by A17, FINSEQ_6:140, NAT_1:12;

A22: p . n = vs1 . n by A15, A19, FINSEQ_6:140;

c1 . n joins vs1 /. n,vs1 /. (n + 1) by A1, A15, A16;

hence (c1 ^ c2) . n joins p /. n,p /. (n + 1) by A12, A13, A14, A20, A18, A22, A21, FINSEQ_1:def 7; :: thesis: verum

end;set v1 = vs1 /. n;

A15: 1 <= n by A14, FINSEQ_3:25;

A16: n <= len c1 by A14, FINSEQ_3:25;

then A17: n + 1 <= len vs1 by A1, XREAL_1:6;

then A18: vs1 /. (n + 1) = vs1 . (n + 1) by FINSEQ_4:15, NAT_1:12;

A19: n <= len vs1 by A6, A16, NAT_1:12;

then A20: vs1 /. n = vs1 . n by A15, FINSEQ_4:15;

A21: p . (n + 1) = vs1 . (n + 1) by A17, FINSEQ_6:140, NAT_1:12;

A22: p . n = vs1 . n by A15, A19, FINSEQ_6:140;

c1 . n joins vs1 /. n,vs1 /. (n + 1) by A1, A15, A16;

hence (c1 ^ c2) . n joins p /. n,p /. (n + 1) by A12, A13, A14, A20, A18, A22, A21, FINSEQ_1:def 7; :: thesis: verum

suppose
ex k being Nat st

( k in dom c2 & n = (len c1) + k ) ; :: thesis: (c1 ^ c2) . b_{1} joins p /. b_{1},p /. (b_{1} + 1)

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

then consider k being Element of NAT such that

A23: k in dom c2 and

A24: n = (len c1) + k ;

A25: 0 + 1 <= k by A23, FINSEQ_3:25;

set v2 = vs2 /. (k + 1);

set v1 = vs2 /. k;

A26: k <= len c2 by A23, FINSEQ_3:25;

then A27: k < len vs2 by A7, NAT_1:13;

A28: 1 <= k by A23, FINSEQ_3:25;

then A29: c2 . k joins vs2 /. k,vs2 /. (k + 1) by A2, A26;

k <= len vs2 by A7, A26, NAT_1:12;

then consider j being Nat such that

0 <= j and

A30: j < len vs2 and

A31: k = j + 1 by A25, FINSEQ_6:127;

A32: p . n = vs2 . k

then A35: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A26, FINSEQ_4:15, XREAL_1:7;

k <= len vs2 by A7, A26, NAT_1:12;

then A36: vs2 /. k = vs2 . k by A28, FINSEQ_4:15;

p . (n + 1) = p . (((len c1) + 1) + k) by A24

.= vs2 . (k + 1) by A6, A28, A27, FINSEQ_6:141 ;

hence (c1 ^ c2) . n joins p /. n,p /. (n + 1) by A12, A13, A23, A24, A36, A35, A29, A32, FINSEQ_1:def 7; :: thesis: verum

end;A23: k in dom c2 and

A24: n = (len c1) + k ;

A25: 0 + 1 <= k by A23, FINSEQ_3:25;

set v2 = vs2 /. (k + 1);

set v1 = vs2 /. k;

A26: k <= len c2 by A23, FINSEQ_3:25;

then A27: k < len vs2 by A7, NAT_1:13;

A28: 1 <= k by A23, FINSEQ_3:25;

then A29: c2 . k joins vs2 /. k,vs2 /. (k + 1) by A2, A26;

k <= len vs2 by A7, A26, NAT_1:12;

then consider j being Nat such that

0 <= j and

A30: j < len vs2 and

A31: k = j + 1 by A25, FINSEQ_6:127;

A32: p . n = vs2 . k

proof
end;

1 <= k + 1
by NAT_1:12;then A35: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A26, FINSEQ_4:15, XREAL_1:7;

k <= len vs2 by A7, A26, NAT_1:12;

then A36: vs2 /. k = vs2 . k by A28, FINSEQ_4:15;

p . (n + 1) = p . (((len c1) + 1) + k) by A24

.= vs2 . (k + 1) by A6, A28, A27, FINSEQ_6:141 ;

hence (c1 ^ c2) . n joins p /. n,p /. (n + 1) by A12, A13, A23, A24, A36, A35, A29, A32, FINSEQ_1:def 7; :: thesis: verum