let G be Graph; for vs1, vs2 being FinSequence of the carrier of G
for c1, c2 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 holds
c1 ^ c2 is oriented Chain of G
let vs1, vs2 be FinSequence of the carrier of G; for c1, c2 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 holds
c1 ^ c2 is oriented Chain of G
let c1, c2 be oriented Chain of G; ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 implies c1 ^ c2 is oriented Chain of G )
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
; c1 ^ c2 is oriented Chain of G
A4:
vs1 is_vertex_seq_of c1
by A1, Th4;
A5:
vs2 is_vertex_seq_of c2
by A2, Th4;
A6:
len vs1 = (len c1) + 1
by A1;
A7:
len vs2 = (len c2) + 1
by A2;
set q = c1 ^ c2;
set p = vs1 ^' vs2;
thus
c1 ^ c2 is oriented Chain of G
verumproof
reconsider cc =
c1 ^ c2 as
Chain of
G by A3, A4, A5, GRAPH_2:43;
for
n being
Nat st 1
<= n &
n < len (c1 ^ c2) holds
the
Source of
G . ((c1 ^ c2) . (n + 1)) = the
Target of
G . ((c1 ^ c2) . n)
proof
let n be
Nat;
( 1 <= n & n < len (c1 ^ c2) implies the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) )
assume that A8:
1
<= n
and A9:
n < len (c1 ^ c2)
;
the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n)
A10:
n in dom (c1 ^ c2)
by A8, A9, FINSEQ_3:25;
A11:
n + 1
<= len (c1 ^ c2)
by A9, NAT_1:13;
A12:
1
< n + 1
by A8, NAT_1:13;
now ( ( n in dom c1 & ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) ) or ( ex k being Nat st
( k in dom c2 & n = (len c1) + k ) & ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) ) )per cases
( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) )
by A10, FINSEQ_1:25;
case A13:
n in dom c1
;
ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 )then A14:
(c1 ^ c2) . n = c1 . n
by FINSEQ_1:def 7;
set v1 =
vs1 /. n;
set v2 =
vs1 /. (n + 1);
A15:
1
<= n
by A13, FINSEQ_3:25;
A16:
n <= len c1
by A13, FINSEQ_3:25;
then A17:
c1 . n orientedly_joins vs1 /. n,
vs1 /. (n + 1)
by A1, A15;
A18:
n <= len vs1
by A6, A16, NAT_1:12;
n + 1
<= (len c1) + 1
by A16, XREAL_1:6;
then A19:
n + 1
<= len vs1
by A1;
A20:
vs1 /. n = vs1 . n
by A15, A18, FINSEQ_4:15;
A21:
vs1 /. (n + 1) = vs1 . (n + 1)
by A19, FINSEQ_4:15, NAT_1:12;
A22:
(vs1 ^' vs2) . n = vs1 . n
by A15, A18, FINSEQ_6:140;
(vs1 ^' vs2) . (n + 1) = vs1 . (n + 1)
by A19, FINSEQ_6:140, NAT_1:12;
hence
ex
v1,
v2 being
Element of
G st
(
v1 = (vs1 ^' vs2) . n &
v2 = (vs1 ^' vs2) . (n + 1) &
(c1 ^ c2) . n orientedly_joins v1,
v2 )
by A14, A17, A20, A21, A22;
verum end; case
ex
k being
Nat st
(
k in dom c2 &
n = (len c1) + k )
;
ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 )then consider k being
Nat such that A23:
k in dom c2
and A24:
n = (len c1) + k
;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
A25:
(c1 ^ c2) . n = c2 . k
by A23, A24, FINSEQ_1:def 7;
A26:
1
<= k
by A23, FINSEQ_3:25;
A27:
k <= len c2
by A23, FINSEQ_3:25;
A28:
1
<= k + 1
by NAT_1:12;
A29:
k <= len vs2
by A7, A27, NAT_1:12;
set v1 =
vs2 /. k;
set v2 =
vs2 /. (k + 1);
A30:
vs2 /. k = vs2 . k
by A26, A29, FINSEQ_4:15;
A31:
vs2 /. (k + 1) = vs2 . (k + 1)
by A7, A27, A28, FINSEQ_4:15, XREAL_1:7;
A32:
c2 . k orientedly_joins vs2 /. k,
vs2 /. (k + 1)
by A2, A26, A27;
A33:
k <= len vs2
by A7, A27, NAT_1:12;
0 + 1
<= k
by A23, FINSEQ_3:25;
then consider j being
Nat such that
0 <= j
and A34:
j < len vs2
and A35:
k = j + 1
by A33, FINSEQ_6:127;
A36:
(vs1 ^' vs2) . n = vs2 . k
A40:
k < len vs2
by A7, A27, NAT_1:13;
(vs1 ^' vs2) . (n + 1) =
(vs1 ^' vs2) . (((len c1) + 1) + k)
by A24
.=
(vs1 ^' vs2) . ((len vs1) + k)
by A1
.=
vs2 . (k + 1)
by A26, 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 orientedly_joins v1,
v2 )
by A25, A30, A31, A32, A36;
verum end; end; end;
then consider v1,
v2 being
Element of
G such that
v1 = (vs1 ^' vs2) . n
and A41:
v2 = (vs1 ^' vs2) . (n + 1)
and A42:
(c1 ^ c2) . n orientedly_joins v1,
v2
;
A43:
n + 1
in dom (c1 ^ c2)
by A11, A12, FINSEQ_3:25;
A44:
now ( ( n + 1 in dom c1 & ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) ) or ( ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) & ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) ) )per cases
( n + 1 in dom c1 or ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) )
by A43, FINSEQ_1:25;
case A45:
n + 1
in dom c1
;
ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 )then A46:
(c1 ^ c2) . (n + 1) = c1 . (n + 1)
by FINSEQ_1:def 7;
set v29 =
vs1 /. (n + 1);
set v3 =
vs1 /. ((n + 1) + 1);
A47:
1
<= n + 1
by A45, FINSEQ_3:25;
A48:
n + 1
<= len c1
by A45, FINSEQ_3:25;
then A49:
c1 . (n + 1) orientedly_joins vs1 /. (n + 1),
vs1 /. ((n + 1) + 1)
by A1, A47;
A50:
n + 1
<= len vs1
by A6, A48, NAT_1:12;
(n + 1) + 1
<= (len c1) + 1
by A48, XREAL_1:6;
then A51:
(n + 1) + 1
<= len vs1
by A1;
A52:
vs1 /. (n + 1) = vs1 . (n + 1)
by A47, A50, FINSEQ_4:15;
A53:
vs1 /. ((n + 1) + 1) = vs1 . ((n + 1) + 1)
by A51, FINSEQ_4:15, NAT_1:12;
A54:
(vs1 ^' vs2) . (n + 1) = vs1 . (n + 1)
by A47, A50, FINSEQ_6:140;
(vs1 ^' vs2) . ((n + 1) + 1) = vs1 . ((n + 1) + 1)
by A51, FINSEQ_6:140, NAT_1:12;
hence
ex
v299,
v39 being
Element of
G st
(
v299 = (vs1 ^' vs2) . (n + 1) &
v39 = (vs1 ^' vs2) . ((n + 1) + 1) &
(c1 ^ c2) . (n + 1) orientedly_joins v299,
v39 )
by A46, A49, A52, A53, A54;
verum end; case
ex
k being
Nat st
(
k in dom c2 &
n + 1
= (len c1) + k )
;
ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 )then consider k being
Nat such that A55:
k in dom c2
and A56:
n + 1
= (len c1) + k
;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
A57:
(c1 ^ c2) . (n + 1) = c2 . k
by A55, A56, FINSEQ_1:def 7;
A58:
1
<= k
by A55, FINSEQ_3:25;
A59:
k <= len c2
by A55, FINSEQ_3:25;
A60:
1
<= k + 1
by NAT_1:12;
A61:
k <= len vs2
by A7, A59, NAT_1:12;
set v29 =
vs2 /. k;
set v3 =
vs2 /. (k + 1);
A62:
vs2 /. k = vs2 . k
by A58, A61, FINSEQ_4:15;
A63:
vs2 /. (k + 1) = vs2 . (k + 1)
by A7, A59, A60, FINSEQ_4:15, XREAL_1:7;
A64:
c2 . k orientedly_joins vs2 /. k,
vs2 /. (k + 1)
by A2, A58, A59;
A65:
k <= len vs2
by A7, A59, NAT_1:12;
0 + 1
<= k
by A55, FINSEQ_3:25;
then consider j being
Nat such that
0 <= j
and A66:
j < len vs2
and A67:
k = j + 1
by A65, FINSEQ_6:127;
A68:
(vs1 ^' vs2) . (n + 1) = vs2 . k
A72:
k < len vs2
by A7, A59, NAT_1:13;
(vs1 ^' vs2) . ((n + 1) + 1) =
(vs1 ^' vs2) . (((len c1) + 1) + k)
by A56
.=
(vs1 ^' vs2) . ((len vs1) + k)
by A1
.=
vs2 . (k + 1)
by A58, A72, FINSEQ_6:141
;
hence
ex
v299,
v39 being
Element of
G st
(
v299 = (vs1 ^' vs2) . (n + 1) &
v39 = (vs1 ^' vs2) . ((n + 1) + 1) &
(c1 ^ c2) . (n + 1) orientedly_joins v299,
v39 )
by A57, A62, A63, A64, A68;
verum end; end; end;
the
Target of
G . ((c1 ^ c2) . n) = v2
by A42;
hence
the
Source of
G . ((c1 ^ c2) . (n + 1)) = the
Target of
G . ((c1 ^ c2) . n)
by A41, A44;
verum
end;
then
cc is
oriented
by GRAPH_1:def 15;
hence
c1 ^ c2 is
oriented Chain of
G
;
verum
end;