let G be Graph; for p being oriented Simple Chain of G
for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Nat holds
( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds
p ^ q is oriented Simple Chain of G
let p be oriented Simple Chain of G; for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Nat holds
( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds
p ^ q is oriented Simple Chain of G
let q be FinSequence of the carrier' of G; ( len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Nat holds
( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) implies p ^ q is oriented Simple Chain of G )
set FS = the Source of G;
set FT = the Target of G;
set v1 = the Source of G . (q . 1);
set v2 = the Target of G . (q . 1);
set vp = the Target of G . (p . (len p));
set E = the carrier' of G;
set V = the carrier of G;
assume that
A1:
len p >= 1
and
A2:
len q = 1
and
A3:
the Source of G . (q . 1) = the Target of G . (p . (len p))
and
A4:
the Source of G . (p . 1) <> the Target of G . (p . (len p))
and
A5:
for k being Nat holds
( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) )
; p ^ q is oriented Simple Chain of G
set lp = len p;
1 in dom q
by A2, FINSEQ_3:25;
then reconsider v1 = the Source of G . (q . 1), v2 = the Target of G . (q . 1) as Element of the carrier of G by FINSEQ_2:11, FUNCT_2:5;
consider r being FinSequence of the carrier of G such that
A6:
r is_oriented_vertex_seq_of p
and
A7:
for n, m being Nat st 1 <= n & n < m & m <= len r & r . n = r . m holds
( n = 1 & m = len r )
by GRAPH_4:def 7;
set pq = p ^ q;
set rv = r ^ <*v2*>;
A8:
len r = (len p) + 1
by A6, GRAPH_4:def 5;
A9:
for n being Nat st 1 <= n & n <= len p holds
p . n joins r /. n,r /. (n + 1)
by A6, GRAPH_4:1, GRAPH_4:def 5;
A10:
now for n being Nat st 1 <= n & n <= len (p ^ q) holds
ex v1, v2 being Element of the carrier of G st
( v1 = (r ^ <*v2*>) . n & v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 )let n be
Nat;
( 1 <= n & n <= len (p ^ q) implies ex v1, v2 being Element of the carrier of G st
( v2 = (r ^ <*v2*>) . v1 & b3 = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b3 ) )assume that A11:
1
<= n
and A12:
n <= len (p ^ q)
;
ex v1, v2 being Element of the carrier of G st
( v2 = (r ^ <*v2*>) . v1 & b3 = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b3 )per cases
( n = len (p ^ q) or n <> len (p ^ q) )
;
suppose A13:
n = len (p ^ q)
;
ex v1, v2 being Element of the carrier of G st
( v2 = (r ^ <*v2*>) . v1 & b3 = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b3 )set m =
len p;
take v1 =
v1;
ex v2 being Element of the carrier of G st
( v1 = (r ^ <*v2*>) . n & v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 )take v2 =
v2;
( v1 = (r ^ <*v2*>) . n & v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 )
p . (len p) orientedly_joins r /. (len p),
r /. ((len p) + 1)
by A1, A6, GRAPH_4:def 5;
then A14:
the
Target of
G . (p . (len p)) = r /. ((len p) + 1)
by GRAPH_4:def 1;
A15:
n = len r
by A2, A8, A13, FINSEQ_1:22;
then
n in dom r
by A11, FINSEQ_3:25;
hence v1 =
r . n
by A3, A8, A15, A14, PARTFUN1:def 6
.=
(r ^ <*v2*>) . n
by A11, A15, Lm1
;
( v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 )thus
v2 = (r ^ <*v2*>) . (n + 1)
by A15, FINSEQ_1:42;
(p ^ q) . n joins v1,v2
q . 1
joins v1,
v2
by GRAPH_1:def 12;
hence
(p ^ q) . n joins v1,
v2
by A2, A8, A15, Lm2;
verum end; suppose A16:
n <> len (p ^ q)
;
ex x, y being Element of the carrier of G st
( y = (r ^ <*v2*>) . x & b3 = (r ^ <*v2*>) . (x + 1) & (p ^ q) . x joins y,b3 )take x =
r /. n;
ex y being Element of the carrier of G st
( x = (r ^ <*v2*>) . n & y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y )take y =
r /. (n + 1);
( x = (r ^ <*v2*>) . n & y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y )
n < len (p ^ q)
by A12, A16, XXREAL_0:1;
then A17:
n < (len p) + 1
by A2, FINSEQ_1:22;
then A18:
n + 1
<= len r
by A8, NAT_1:13;
n in dom r
by A8, A11, A17, FINSEQ_3:25;
hence x =
r . n
by PARTFUN1:def 6
.=
(r ^ <*v2*>) . n
by A8, A11, A17, Lm1
;
( y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y )
1
<= n + 1
by NAT_1:12;
then
n + 1
in dom r
by A18, FINSEQ_3:25;
hence y =
r . (n + 1)
by PARTFUN1:def 6
.=
(r ^ <*v2*>) . (n + 1)
by A18, Lm1, NAT_1:12
;
(p ^ q) . n joins x,yA19:
n <= len p
by A17, NAT_1:13;
then
p . n joins r /. n,
r /. (n + 1)
by A9, A11;
hence
(p ^ q) . n joins x,
y
by A11, A19, Lm1;
verum end; end; end;
A22:
len (r ^ <*v2*>) = (len r) + 1
by FINSEQ_2:16;
then A23:
len (r ^ <*v2*>) = (len (p ^ q)) + 1
by A2, A8, FINSEQ_1:22;
p . (len p) orientedly_joins r /. (len p),r /. ((len p) + 1)
by A1, A6, GRAPH_4:def 5;
then A24:
the Target of G . (p . (len p)) = r /. ((len p) + 1)
by GRAPH_4:def 1;
A25:
now for n, m being Nat st 1 <= n & n < m & m <= len (r ^ <*v2*>) & (r ^ <*v2*>) . n = (r ^ <*v2*>) . m holds
( n = 1 & m = len (r ^ <*v2*>) )let n,
m be
Nat;
( 1 <= n & n < m & m <= len (r ^ <*v2*>) & (r ^ <*v2*>) . n = (r ^ <*v2*>) . m implies ( n = 1 & m = len (r ^ <*v2*>) ) )assume that A26:
1
<= n
and A27:
n < m
and A28:
m <= len (r ^ <*v2*>)
and A29:
(r ^ <*v2*>) . n = (r ^ <*v2*>) . m
;
( n = 1 & m = len (r ^ <*v2*>) )assume A30:
( not
n = 1 or not
m = len (r ^ <*v2*>) )
;
contradictionper cases
( m < len (r ^ <*v2*>) or m >= len (r ^ <*v2*>) )
;
suppose
m < len (r ^ <*v2*>)
;
contradictionthen A31:
m <= len r
by A22, NAT_1:13;
A32:
1
<= m
by A26, A27, XXREAL_0:2;
then A33:
m in dom r
by A31, FINSEQ_3:25;
n < len r
by A27, A31, XXREAL_0:2;
then A34:
r . n =
(r ^ <*v2*>) . n
by A26, Lm1
.=
r . m
by A29, A31, A32, Lm1
;
then A35:
m = len r
by A7, A26, A27, A31;
A36:
n = 1
by A7, A26, A27, A31, A34;
then A37:
1
in dom r
by A27, A35, FINSEQ_3:25;
p . 1
orientedly_joins r /. 1,
r /. (1 + 1)
by A1, A6, GRAPH_4:def 5;
then the
Source of
G . (p . 1) =
r /. 1
by GRAPH_4:def 1
.=
r . m
by A34, A36, A37, PARTFUN1:def 6
.=
the
Target of
G . (p . (len p))
by A8, A24, A35, A33, PARTFUN1:def 6
;
hence
contradiction
by A4;
verum end; suppose A38:
m >= len (r ^ <*v2*>)
;
contradictionthen
m = len (r ^ <*v2*>)
by A28, XXREAL_0:1;
then A39:
v2 = (r ^ <*v2*>) . m
by A22, FINSEQ_1:42;
consider k being
Nat such that A40:
n = k + 1
by A26, NAT_1:6;
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
1
< n
by A26, A28, A30, A38, XXREAL_0:1;
then A41:
1
<= k
by A40, NAT_1:13;
k + 1
< (len r) + 1
by A22, A27, A28, A40, XXREAL_0:2;
then A42:
k + 1
<= len r
by NAT_1:13;
then A43:
k + 1
in dom r
by A26, A40, FINSEQ_3:25;
A44:
k <= len p
by A8, A42, XREAL_1:6;
then
p . k orientedly_joins r /. k,
r /. (k + 1)
by A6, A41, GRAPH_4:def 5;
then the
Target of
G . (p . k) =
r /. (k + 1)
by GRAPH_4:def 1
.=
r . (k + 1)
by A43, PARTFUN1:def 6
.=
v2
by A26, A29, A39, A40, A42, Lm1
;
hence
contradiction
by A5, A41, A44;
verum end; end; end;
now for n being Nat st 1 <= n & n <= len (p ^ q) holds
(p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,(r ^ <*v2*>) /. (n + 1)A56:
dom r c= dom (r ^ <*v2*>)
by FINSEQ_1:26;
let n be
Nat;
( 1 <= n & n <= len (p ^ q) implies (p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1) )assume that A57:
1
<= n
and A58:
n <= len (p ^ q)
;
(p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1)per cases
( n <= len p or n > len p )
;
suppose A59:
n <= len p
;
(p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1)then A60:
n + 1
<= len r
by A8, XREAL_1:7;
1
<= n + 1
by NAT_1:12;
then A61:
n + 1
in dom r
by A60, FINSEQ_3:25;
then A62:
r /. (n + 1) =
r . (n + 1)
by PARTFUN1:def 6
.=
(r ^ <*v2*>) . (n + 1)
by A60, Lm1, NAT_1:12
.=
(r ^ <*v2*>) /. (n + 1)
by A56, A61, PARTFUN1:def 6
;
A63:
p . n orientedly_joins r /. n,
r /. (n + 1)
by A6, A57, A59, GRAPH_4:def 5;
A64:
n <= len r
by A8, A59, NAT_1:12;
then A65:
n in dom r
by A57, FINSEQ_3:25;
then r /. n =
r . n
by PARTFUN1:def 6
.=
(r ^ <*v2*>) . n
by A57, A64, Lm1
.=
(r ^ <*v2*>) /. n
by A56, A65, PARTFUN1:def 6
;
hence
(p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,
(r ^ <*v2*>) /. (n + 1)
by A57, A59, A63, A62, Lm1;
verum end; suppose A66:
n > len p
;
(p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1)A67:
(len p) + 1
>= n
by A2, A58, FINSEQ_1:22;
(len p) + 1
<= n
by A66, NAT_1:13;
then A68:
n = len r
by A8, A67, XXREAL_0:1;
1
<= n + 1
by NAT_1:12;
then A69:
n + 1
in dom (r ^ <*v2*>)
by A22, A68, FINSEQ_3:25;
A70:
v2 =
(r ^ <*v2*>) . (n + 1)
by A68, FINSEQ_1:42
.=
(r ^ <*v2*>) /. (n + 1)
by A69, PARTFUN1:def 6
;
A71:
q . 1
orientedly_joins v1,
v2
by GRAPH_4:def 1;
A72:
n in dom r
by A8, A57, A67, FINSEQ_3:25;
then v1 =
r . n
by A3, A8, A24, A68, PARTFUN1:def 6
.=
(r ^ <*v2*>) . n
by A8, A57, A67, Lm1
.=
(r ^ <*v2*>) /. n
by A56, A72, PARTFUN1:def 6
;
hence
(p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,
(r ^ <*v2*>) /. (n + 1)
by A2, A8, A68, A70, A71, Lm2;
verum end; end; end;
then
r ^ <*v2*> is_oriented_vertex_seq_of p ^ q
by A23, GRAPH_4:def 5;
hence
p ^ q is oriented Simple Chain of G
by A20, A23, A52, A10, A45, A25, GRAPH_1:def 14, GRAPH_1:def 15, GRAPH_4:def 7; verum