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 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, Def7;
A7: len vs2 = (len c2) + 1 by A2, Def7;
then vs2 <> {} ;
then (len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by Th13;
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
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b1 joins p /. b1,p /. (b1 + 1) )
assume that
A9: 1 <= n and
A10: n <= len (c1 ^ c2) ; :: thesis: (c1 ^ c2) . b1 joins p /. b1,p /. (b1 + 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;
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;
suppose A14: n in dom c1 ; :: thesis: (c1 ^ c2) . b1 joins p /. b1,p /. (b1 + 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 n + 1 <= (len c1) + 1 by XREAL_1:6;
then A17: n + 1 <= len vs1 by A1, Def7;
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, Th14, NAT_1:12;
A22: p . n = vs1 . n by A15, A19, Th14;
c1 . n joins vs1 /. n,vs1 /. (n + 1) by A1, A15, A16, Def7;
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;
suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis: (c1 ^ c2) . b1 joins p /. b1,p /. (b1 + 1)
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, Def7;
k <= len vs2 by A7, A26, NAT_1:12;
then consider j being Element of NAT such that
0 <= j and
A30: j < len vs2 and
A31: k = j + 1 by A25, Th1;
A32: p . n = vs2 . k
proof
per cases ( 1 = k or 1 < k ) by A28, XXREAL_0:1;
suppose A33: 1 = k ; :: thesis: p . n = vs2 . k
0 + 1 <= len vs1 by A6, NAT_1:13;
hence p . n = vs2 . k by A3, A6, A24, A33, Th14; :: thesis: verum
end;
suppose 1 < k ; :: thesis: p . n = vs2 . k
then A34: 1 <= j by A31, NAT_1:13;
thus p . n = p . ((len vs1) + j) by A6, A24, A31
.= vs2 . k by A30, A31, A34, Th15 ; :: thesis: verum
end;
end;
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, Th15 ;
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;
end;
end;
hence vs is_vertex_seq_of c by A4, A5, A8, Def7; :: thesis: verum