let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: 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 :: thesis: 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; :: thesis: ( 1 <= n & n <= len (p ^ q) implies ex v1, v2 being Element of the carrier of G st
( v2 = (r ^ <*v2*>) . v1 & b₃ = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b₃ ) )
assume that
A11: 1 <= n and
A12: n <= len (p ^ q) ; :: thesis: ex v1, v2 being Element of the carrier of G st
( v2 = (r ^ <*v2*>) . v1 & b₃ = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b₃ )

per cases ( n = len (p ^ q) or n <> len (p ^ q) ) ;

suppose A13: n = len (p ^ q) ; :: thesis: ex v1, v2 being Element of the carrier of G st
( v2 = (r ^ <*v2*>) . v1 & b₃ = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b₃ )

set m = len p;
take v1 = v1; :: thesis: 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; :: thesis: ( 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 ;
:: thesis: ( v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 )
thus v2 = (r ^ <*v2*>) . (n + 1) by A15, FINSEQ_1:42; :: thesis: (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; :: thesis: verum

end;

suppose A16: n <> len (p ^ q) ; :: thesis: ex x, y being Element of the carrier of G st
( y = (r ^ <*v2*>) . x & b₃ = (r ^ <*v2*>) . (x + 1) & (p ^ q) . x joins y,b₃ )

take x = r /. n; :: thesis: 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); :: thesis: ( 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 ;
:: thesis: ( 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 ;
:: thesis: (p ^ q) . n joins x,y
A19: 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; :: thesis: verum

end;

end;

end;

A20: now :: thesis: for n being Nat st 1 <= n & n <= len (p ^ q) holds
(p ^ q) . n in the carrier' of G

let n be Nat; :: thesis: ( 1 <= n & n <= len (p ^ q) implies (p ^ q) . n in the carrier' of G )
assume ( 1 <= n & n <= len (p ^ q) ) ; :: thesis: (p ^ q) . n in the carrier' of G
then n in dom (p ^ q) by FINSEQ_3:25;
then (p ^ q) . n in rng (p ^ q) by FUNCT_1:def 3;
then A21: (p ^ q) . n in (rng p) \/ (rng q) by FINSEQ_1:31;
( rng p c= the carrier' of G & rng q c= the carrier' of G ) by FINSEQ_1:def 4;
then (rng p) \/ (rng q) c= the carrier' of G by XBOOLE_1:8;
hence (p ^ q) . n in the carrier' of G by A21; :: thesis: verum

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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( n = 1 & m = len (r ^ <*v2*>) )
assume A30: ( not n = 1 or not m = len (r ^ <*v2*>) ) ; :: thesis: contradiction

per cases ( m < len (r ^ <*v2*>) or m >= len (r ^ <*v2*>) ) ;

suppose m < len (r ^ <*v2*>) ; :: thesis: contradiction

then 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; :: thesis: verum

end;

suppose A38: m >= len (r ^ <*v2*>) ; :: thesis: contradiction

then 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; :: thesis: verum

end;

end;

end;

A45: now :: thesis: for n being Nat st 1 <= n & n < len (p ^ q) holds
the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n)

let n be Nat; :: thesis: ( 1 <= n & n < len (p ^ q) implies the Source of G . ((p ^ q) . (b₁ + 1)) = the Target of G . ((p ^ q) . b₁) )
assume that
A46: 1 <= n and
A47: n < len (p ^ q) ; :: thesis: the Source of G . ((p ^ q) . (b₁ + 1)) = the Target of G . ((p ^ q) . b₁)

per cases ( n < len p or n >= len p ) ;

suppose A48: n < len p ; :: thesis: the Source of G . ((p ^ q) . (b₁ + 1)) = the Target of G . ((p ^ q) . b₁)

then A49: n + 1 <= len p by NAT_1:13;
( the Source of G . (p . (n + 1)) = the Target of G . (p . n) & p . n = (p ^ q) . n ) by A46, A48, Lm1, GRAPH_1:def 15;
hence the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A49, Lm1, NAT_1:12; :: thesis: verum

end;

suppose A50: n >= len p ; :: thesis: the Source of G . ((p ^ q) . (b₁ + 1)) = the Target of G . ((p ^ q) . b₁)

n < (len p) + 1 by A2, A47, FINSEQ_1:22;
then n <= len p by NAT_1:13;
then A51: n = len p by A50, XXREAL_0:1;
then (p ^ q) . n = p . (len p) by A1, Lm1;
hence the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A2, A3, A51, Lm2; :: thesis: verum

end;

end;

end;

A52: now :: thesis: for n being Nat st 1 <= n & n <= len (r ^ <*v2*>) holds
(r ^ <*v2*>) . n in the carrier of G

let n be Nat; :: thesis: ( 1 <= n & n <= len (r ^ <*v2*>) implies (r ^ <*v2*>) . b₁ in the carrier of G )
assume that
A53: 1 <= n and
A54: n <= len (r ^ <*v2*>) ; :: thesis: (r ^ <*v2*>) . b₁ in the carrier of G

per cases ( n = len (r ^ <*v2*>) or n <> len (r ^ <*v2*>) ) ;

suppose n = len (r ^ <*v2*>) ; :: thesis: (r ^ <*v2*>) . b₁ in the carrier of G

then (r ^ <*v2*>) . n = v2 by A22, FINSEQ_1:42;
hence (r ^ <*v2*>) . n in the carrier of G ; :: thesis: verum

end;

suppose n <> len (r ^ <*v2*>) ; :: thesis: (r ^ <*v2*>) . b₁ in the carrier of G

then n < len (r ^ <*v2*>) by A54, XXREAL_0:1;
then A55: n <= len r by A22, NAT_1:13;
then n in dom r by A53, FINSEQ_3:25;
then r . n in the carrier of G by FINSEQ_2:11;
hence (r ^ <*v2*>) . n in the carrier of G by A53, A55, Lm1; :: thesis: verum

end;

end;

end;

now :: thesis: 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; :: thesis: ( 1 <= n & n <= len (p ^ q) implies (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 1) )
assume that
A57: 1 <= n and
A58: n <= len (p ^ q) ; :: thesis: (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 1)

per cases ( n <= len p or n > len p ) ;

suppose A59: n <= len p ; :: thesis: (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 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; :: thesis: verum

end;

suppose A66: n > len p ; :: thesis: (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 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; :: thesis: 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; :: thesis: verum