let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 )
; :: thesis: ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_oriented_vertex_seq_of c )
assume A2:
( c = c1 ^ c2 & vs = vs1 ^' vs2 )
; :: thesis: vs is_oriented_vertex_seq_of c
A3:
( len vs1 = (len c1) + 1 & len vs2 = (len c2) + 1 )
by A1, Def5;
then A4:
( vs1 <> {} & vs2 <> {} )
;
set q = c1 ^ c2;
set p = vs1 ^' vs2;
(len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2)
by A4, GRAPH_2:13;
then A5: len (vs1 ^' vs2) =
((len c1) + (len c2)) + 1
by A3
.=
(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 ;
:: thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) )assume A6:
( 1
<= n &
n <= len (c1 ^ c2) )
;
:: thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)then
(
n <= len p & 1
<= n + 1 &
n + 1
<= len p )
by A5, NAT_1:12, XREAL_1:9;
then A7:
(
p /. n = p . n &
p /. (n + 1) = p . (n + 1) )
by A6, FINSEQ_4:24;
A8:
n in dom (c1 ^ c2)
by A6, FINSEQ_3:27;
per cases
( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) )
by A8, FINSEQ_1:38;
suppose A9:
n in dom c1
;
:: thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)set v1 =
vs1 /. n;
set v2 =
vs1 /. (n + 1);
A10:
( 1
<= n &
n <= len c1 )
by A9, FINSEQ_3:27;
then A11:
c1 . n orientedly_joins vs1 /. n,
vs1 /. (n + 1)
by A1, Def5;
A12:
n <= len vs1
by A3, A10, NAT_1:12;
( 1
<= n + 1 &
n + 1
<= (len c1) + 1 )
by A10, NAT_1:12, XREAL_1:8;
then A13:
( 1
<= n + 1 &
n + 1
<= len vs1 )
by A1, Def5;
then A14:
(
vs1 /. n = vs1 . n &
vs1 /. (n + 1) = vs1 . (n + 1) )
by A10, A12, FINSEQ_4:24;
(
p . n = vs1 . n &
p . (n + 1) = vs1 . (n + 1) )
by A10, A12, A13, GRAPH_2:14;
hence
(c1 ^ c2) . n orientedly_joins p /. n,
p /. (n + 1)
by A7, A9, A11, A14, 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 orientedly_joins p /. b1,p /. (b1 + 1)then consider k being
Nat such that A15:
(
k in dom c2 &
n = (len c1) + k )
;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 13;
A16:
(c1 ^ c2) . n = c2 . k
by A15, FINSEQ_1:def 7;
A17:
( 1
<= k &
k <= len c2 )
by A15, FINSEQ_3:27;
then
( 1
<= k + 1 &
k <= len vs2 &
k + 1
<= len vs2 )
by A3, NAT_1:12, XREAL_1:9;
then A18:
(
vs2 /. k = vs2 . k &
vs2 /. (k + 1) = vs2 . (k + 1) )
by A17, FINSEQ_4:24;
A19:
k <= len vs2
by A3, A17, NAT_1:12;
0 + 1
<= k
by A15, FINSEQ_3:27;
then consider j being
Element of
NAT such that A20:
(
0 <= j &
j < len vs2 &
k = j + 1 )
by A19, GRAPH_2:1;
A21:
p . n = vs2 . k
A25:
k < len vs2
by A3, A17, NAT_1:13;
p . (n + 1) =
p . (((len c1) + 1) + k)
by A15
.=
p . ((len vs1) + k)
by A1, Def5
.=
vs2 . (k + 1)
by A17, A25, GRAPH_2:15
;
hence
(c1 ^ c2) . n orientedly_joins p /. n,
p /. (n + 1)
by A1, A7, A16, A17, A18, A21, Def5;
:: thesis: verum end; end;
hence
vs is_oriented_vertex_seq_of c
by A2, A5, Def5; :: thesis: verum