let G be Graph; 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; 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; ( 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
; 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;
A16:
len vs1 = (len c1) + 1
by A1;
A17:
now 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;
( 1 <= n & n <= len (c1 ^ c2) implies ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b3 = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b3 ) )assume that A18:
1
<= n
and A19:
n <= len (c1 ^ c2)
;
ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b3 = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b3 )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
;
ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b3 = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b3 )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;
verum end; suppose
ex
k being
Nat st
(
k in dom c2 &
n = (len c1) + k )
;
ex v1, v2 being Element of G st
( v2 = (vs1 ^' vs2) . v1 & b3 = (vs1 ^' vs2) . (v1 + 1) & (c1 ^ c2) . v1 joins v2,b3 )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 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;
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
verum