let G be Graph; for vs1, vs2, vs being FinSequence of the carrier of G
for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_oriented_vertex_seq_of c
let vs1, vs2, vs be FinSequence of the carrier of G; for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_oriented_vertex_seq_of c
let c1, c2, c be oriented Chain of G; ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 implies vs is_oriented_vertex_seq_of c )
assume that
A1:
vs1 is_oriented_vertex_seq_of c1
and
A2:
vs2 is_oriented_vertex_seq_of c2
and
A3:
vs1 . (len vs1) = vs2 . 1
; ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_oriented_vertex_seq_of c )
assume that
A4:
c = c1 ^ c2
and
A5:
vs = vs1 ^' vs2
; vs is_oriented_vertex_seq_of c
A6:
len vs1 = (len c1) + 1
by A1, Def5;
A7:
len vs2 = (len c2) + 1
by A2, Def5;
then A8:
vs2 <> {}
;
set q = c1 ^ c2;
set p = vs1 ^' vs2;
(len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2)
by A8, GRAPH_2:13;
then A9: len (vs1 ^' vs2) =
((len c1) + (len c2)) + 1
by A6, A7
.=
(len (c1 ^ c2)) + 1
by FINSEQ_1:35
;
reconsider p = vs1 ^' vs2 as FinSequence of the carrier of G ;
now let n be
Element of
NAT ;
( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) )assume that A10:
1
<= n
and A11:
n <= len (c1 ^ c2)
;
(c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)A12:
n <= len p
by A9, A11, NAT_1:12;
A13:
1
<= n + 1
by NAT_1:12;
A14:
p /. n = p . n
by A10, A12, FINSEQ_4:24;
A15:
p /. (n + 1) = p . (n + 1)
by A9, A11, A13, FINSEQ_4:24, XREAL_1:9;
A16:
n in dom (c1 ^ c2)
by A10, A11, FINSEQ_3:27;
per cases
( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) )
by A16, FINSEQ_1:38;
suppose A17:
n in dom c1
;
(c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)set v1 =
vs1 /. n;
set v2 =
vs1 /. (n + 1);
A18:
1
<= n
by A17, FINSEQ_3:27;
A19:
n <= len c1
by A17, FINSEQ_3:27;
then A20:
c1 . n orientedly_joins vs1 /. n,
vs1 /. (n + 1)
by A1, A18, Def5;
A21:
n <= len vs1
by A6, A19, NAT_1:12;
n + 1
<= (len c1) + 1
by A19, XREAL_1:8;
then A22:
n + 1
<= len vs1
by A1, Def5;
A23:
vs1 /. n = vs1 . n
by A18, A21, FINSEQ_4:24;
A24:
vs1 /. (n + 1) = vs1 . (n + 1)
by A22, FINSEQ_4:24, NAT_1:12;
A25:
p . n = vs1 . n
by A18, A21, GRAPH_2:14;
p . (n + 1) = vs1 . (n + 1)
by A22, GRAPH_2:14, NAT_1:12;
hence
(c1 ^ c2) . n orientedly_joins p /. n,
p /. (n + 1)
by A14, A15, A17, A20, A23, A24, A25, FINSEQ_1:def 7;
verum end; suppose
ex
k being
Nat st
(
k in dom c2 &
n = (len c1) + k )
;
(c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)then consider k being
Nat such that A26:
k in dom c2
and A27:
n = (len c1) + k
;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
A28:
(c1 ^ c2) . n = c2 . k
by A26, A27, FINSEQ_1:def 7;
A29:
1
<= k
by A26, FINSEQ_3:27;
A30:
k <= len c2
by A26, FINSEQ_3:27;
A31:
1
<= k + 1
by NAT_1:12;
k <= len vs2
by A7, A30, NAT_1:12;
then A32:
vs2 /. k = vs2 . k
by A29, FINSEQ_4:24;
A33:
vs2 /. (k + 1) = vs2 . (k + 1)
by A7, A30, A31, FINSEQ_4:24, XREAL_1:9;
A34:
k <= len vs2
by A7, A30, NAT_1:12;
0 + 1
<= k
by A26, FINSEQ_3:27;
then consider j being
Element of
NAT such that
0 <= j
and A35:
j < len vs2
and A36:
k = j + 1
by A34, GRAPH_2:1;
A37:
p . n = vs2 . k
A41:
k < len vs2
by A7, A30, NAT_1:13;
p . (n + 1) =
p . (((len c1) + 1) + k)
by A27
.=
p . ((len vs1) + k)
by A1, Def5
.=
vs2 . (k + 1)
by A29, A41, GRAPH_2:15
;
hence
(c1 ^ c2) . n orientedly_joins p /. n,
p /. (n + 1)
by A2, A14, A15, A28, A29, A30, A32, A33, A37, Def5;
verum end; end;
hence
vs is_oriented_vertex_seq_of c
by A4, A5, A9, Def5; verum