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 Element of 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 Element of 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 Element of 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 A1: ( 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 Element of 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
consider r being FinSequence of the carrier of G such that
A2: ( r is_oriented_vertex_seq_of p & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len r & r . n = r . m holds
( n = 1 & m = len r ) ) ) by GRAPH_4:def 7;
A3: ( len r = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n orientedly_joins r /. n,r /. (n + 1) ) ) by A2, GRAPH_4:def 5;

A4: now

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len p implies p . n joins r /. n,r /. (n + 1) )
assume ( 1 <= n & n <= len p ) ; :: thesis: p . n joins r /. n,r /. (n + 1)
then p . n orientedly_joins r /. n,r /. (n + 1) by A2, GRAPH_4:def 5;
hence p . n joins r /. n,r /. (n + 1) by GRAPH_4:1; :: thesis: verum

end;

set pq = p ^ q;

A5: now

let n be Element of 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:27;
then (p ^ q) . n in rng (p ^ q) by FUNCT_1:def 5;
then A6: (p ^ q) . n in (rng p) \/ (rng q) by FINSEQ_1:44;
( 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 A6; :: thesis: verum

end;

1 in dom q by A1, FINSEQ_3:27;
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:13, FUNCT_2:7;
set rv = r ^ <*v2*>;
A7: len (r ^ <*v2*>) = (len r) + 1 by FINSEQ_2:19;
then A8: len (r ^ <*v2*>) = (len (p ^ q)) + 1 by A1, A3, FINSEQ_1:35;

A9: now

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (r ^ <*v2*>) implies (r ^ <*v2*>) . b₁ in the carrier of G )
assume A10: ( 1 <= n & 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 A7, FINSEQ_1:59;
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 A10, XXREAL_0:1;
then A11: n <= len r by A7, NAT_1:13;
then n in dom r by A10, FINSEQ_3:27;
then r . n in the carrier of G by FINSEQ_2:13;
hence (r ^ <*v2*>) . n in the carrier of G by A10, A11, Lm1; :: thesis: verum

end;

end;

end;

A12: now

let n be Element of 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 A13: ( 1 <= n & 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 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₃ )

then A14: n = len r by A1, A3, FINSEQ_1:35;
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 )
set m = len p;
A15: n in dom r by A13, A14, FINSEQ_3:27;
p . (len p) orientedly_joins r /. (len p),r /. ((len p) + 1) by A1, A2, GRAPH_4:def 5;
then the Target of G . (p . (len p)) = r /. ((len p) + 1) by GRAPH_4:def 1;
hence v1 = r . n by A1, A3, A14, A15, PARTFUN1:def 8
.= (r ^ <*v2*>) . n by A13, A14, Lm1 ;
:: thesis: ( v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 )
thus v2 = (r ^ <*v2*>) . (n + 1) by A14, FINSEQ_1:59; :: thesis: (p ^ q) . n joins v1,v2
q . 1 joins v1,v2 by GRAPH_1:def 10;
hence (p ^ q) . n joins v1,v2 by A1, A3, A14, Lm2; :: thesis: verum

end;

suppose 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₃ )

then n < len (p ^ q) by A13, XXREAL_0:1;
then A16: n < (len p) + 1 by A1, FINSEQ_1:35;
then A17: n <= len p by NAT_1:13;
then A18: p . n joins r /. n,r /. (n + 1) by A4, A13;
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 in dom r by A3, A13, A16, FINSEQ_3:27;
hence x = r . n by PARTFUN1:def 8
.= (r ^ <*v2*>) . n by A3, A13, A16, Lm1 ;
:: thesis: ( y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y )
A19: 1 <= n + 1 by NAT_1:12;
A20: n + 1 <= len r by A3, A16, NAT_1:13;
then n + 1 in dom r by A19, FINSEQ_3:27;
hence y = r . (n + 1) by PARTFUN1:def 8
.= (r ^ <*v2*>) . (n + 1) by A20, Lm1, NAT_1:12 ;
:: thesis: (p ^ q) . n joins x,y
thus (p ^ q) . n joins x,y by A13, A17, A18, Lm1; :: thesis: verum

end;

end;

end;

A21: now

let n be Element of 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 A22: ( 1 <= n & 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 A23: n < len p ; :: thesis: the Source of G . ((p ^ q) . (b₁ + 1)) = the Target of G . ((p ^ q) . b₁)

then A24: the Source of G . (p . (n + 1)) = the Target of G . (p . n) by A22, GRAPH_1:def 13;
A25: p . n = (p ^ q) . n by A22, A23, Lm1;
n + 1 <= len p by A23, NAT_1:13;
hence the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A24, A25, Lm1, NAT_1:12; :: thesis: verum

end;

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

n < (len p) + 1 by A1, A22, FINSEQ_1:35;
then n <= len p by NAT_1:13;
then A27: n = len p by A26, 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 A1, A27, Lm2; :: thesis: verum

end;

end;

end;

set lp = len p;
p . (len p) orientedly_joins r /. (len p),r /. ((len p) + 1) by A1, A2, GRAPH_4:def 5;
then A28: the Target of G . (p . (len p)) = r /. ((len p) + 1) by GRAPH_4:def 1;

now

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (p ^ q) implies (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 1) )
assume A29: ( 1 <= n & n <= len (p ^ q) ) ; :: thesis: (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 1)
A30: dom r c= dom (r ^ <*v2*>) by FINSEQ_1:39;

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

suppose A31: n <= len p ; :: thesis: (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 1)

then A32: p . n orientedly_joins r /. n,r /. (n + 1) by A2, A29, GRAPH_4:def 5;
A33: n <= len r by A3, A31, NAT_1:12;
then A34: n in dom r by A29, FINSEQ_3:27;
then A35: r /. n = r . n by PARTFUN1:def 8
.= (r ^ <*v2*>) . n by A29, A33, Lm1
.= (r ^ <*v2*>) /. n by A30, A34, PARTFUN1:def 8 ;
A36: n + 1 <= len r by A3, A31, XREAL_1:9;
1 <= n + 1 by NAT_1:12;
then A37: n + 1 in dom r by A36, FINSEQ_3:27;
then r /. (n + 1) = r . (n + 1) by PARTFUN1:def 8
.= (r ^ <*v2*>) . (n + 1) by A36, Lm1, NAT_1:12
.= (r ^ <*v2*>) /. (n + 1) by A30, A37, PARTFUN1:def 8 ;
hence (p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,(r ^ <*v2*>) /. (n + 1) by A29, A31, A32, A35, Lm1; :: thesis: verum

end;

suppose n > len p ; :: thesis: (p ^ q) . b₁ orientedly_joins (r ^ <*v2*>) /. b₁,(r ^ <*v2*>) /. (b₁ + 1)

then A38: (len p) + 1 <= n by NAT_1:13;
A39: (len p) + 1 >= n by A1, A29, FINSEQ_1:35;
then A40: n = len r by A3, A38, XXREAL_0:1;
A41: n in dom r by A3, A29, A39, FINSEQ_3:27;
1 <= n + 1 by NAT_1:12;
then A42: n + 1 in dom (r ^ <*v2*>) by A7, A40, FINSEQ_3:27;
A43: v1 = r . n by A1, A3, A28, A40, A41, PARTFUN1:def 8
.= (r ^ <*v2*>) . n by A3, A29, A39, Lm1
.= (r ^ <*v2*>) /. n by A30, A41, PARTFUN1:def 8 ;
A44: v2 = (r ^ <*v2*>) . (n + 1) by A40, FINSEQ_1:59
.= (r ^ <*v2*>) /. (n + 1) by A42, PARTFUN1:def 8 ;
q . 1 orientedly_joins v1,v2 by GRAPH_4:def 1;
hence (p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,(r ^ <*v2*>) /. (n + 1) by A1, A3, A40, A43, A44, Lm2; :: thesis: verum

end;

end;

end;

then A45: r ^ <*v2*> is_oriented_vertex_seq_of p ^ q by A8, GRAPH_4:def 5;

now

let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len (r ^ <*v2*>) & (r ^ <*v2*>) . n = (r ^ <*v2*>) . m implies ( n = 1 & m = len (r ^ <*v2*>) ) )
assume A46: ( 1 <= n & n < m & m <= len (r ^ <*v2*>) & (r ^ <*v2*>) . n = (r ^ <*v2*>) . m ) ; :: thesis: ( n = 1 & m = len (r ^ <*v2*>) )
assume A47: ( 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 A48: m <= len r by A7, NAT_1:13;
then A49: n < len r by A46, XXREAL_0:2;
A50: 1 <= m by A46, XXREAL_0:2;
A51: r . n = (r ^ <*v2*>) . n by A46, A49, Lm1
.= r . m by A46, A48, A50, Lm1 ;
then A52: ( n = 1 & m = len r ) by A2, A46, A48;
then A53: 1 in dom r by A46, FINSEQ_3:27;
A54: m in dom r by A48, A50, FINSEQ_3:27;
p . 1 orientedly_joins r /. 1,r /. (1 + 1) by A1, A2, GRAPH_4:def 5;
then the Source of G . (p . 1) = r /. 1 by GRAPH_4:def 1
.= r . m by A51, A52, A53, PARTFUN1:def 8
.= the Target of G . (p . (len p)) by A3, A28, A52, A54, PARTFUN1:def 8 ;
hence contradiction by A1; :: thesis: verum

end;

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

then m = len (r ^ <*v2*>) by A46, XXREAL_0:1;
then A56: v2 = (r ^ <*v2*>) . m by A7, FINSEQ_1:59;
A57: 1 < n by A46, A47, A55, XXREAL_0:1;
consider k being Nat such that
A58: n = k + 1 by A46, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A59: 1 <= k by A57, A58, NAT_1:13;
k + 1 < (len r) + 1 by A7, A46, A58, XXREAL_0:2;
then A60: k + 1 <= len r by NAT_1:13;
then A61: k <= len p by A3, XREAL_1:8;
A62: k + 1 in dom r by A46, A58, A60, FINSEQ_3:27;
p . k orientedly_joins r /. k,r /. (k + 1) by A2, A59, A61, GRAPH_4:def 5;
then the Target of G . (p . k) = r /. (k + 1) by GRAPH_4:def 1
.= r . (k + 1) by A62, PARTFUN1:def 8
.= v2 by A46, A56, A58, A60, Lm1 ;
hence contradiction by A1, A59, A61; :: thesis: verum

end;

end;

end;

hence p ^ q is oriented Simple Chain of G by A5, A8, A9, A12, A21, A45, GRAPH_1:def 12, GRAPH_1:def 13, GRAPH_4:def 7; :: thesis: verum