let G be Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: verum

proof

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

end;

case ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis: 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

proof

per cases ( 1 = k or 1 < k ) by A26, XXREAL_0:1;

suppose A37: 1 = k ; :: thesis: (vs1 ^' vs2) . n = vs2 . k

A38: 0 + 1 <= len vs1 by A6, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (len vs1) by A1, A24, A37
.= vs2 . k by A3, A37, A38, FINSEQ_6:140 ; :: thesis: verum

end;

suppose 1 < k ; :: thesis: (vs1 ^' vs2) . n = vs2 . k

then A39: 1 <= j by A35, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (((len c1) + 1) + j) by A24, A35
.= (vs1 ^' vs2) . ((len vs1) + j) by A1
.= vs2 . k by A34, A35, A39, FINSEQ_6:141 ; :: thesis: verum

end;

end;

end;

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

end;

case ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) ; :: thesis: 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

proof

per cases ( 1 = k or 1 < k ) by A58, XXREAL_0:1;

suppose A69: 1 = k ; :: thesis: (vs1 ^' vs2) . (n + 1) = vs2 . k

A70: 0 + 1 <= len vs1 by A6, NAT_1:13;
thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (len vs1) by A1, A56, A69
.= vs2 . k by A3, A69, A70, FINSEQ_6:140 ; :: thesis: verum

end;

suppose 1 < k ; :: thesis: (vs1 ^' vs2) . (n + 1) = vs2 . k

then A71: 1 <= j by A67, NAT_1:13;
thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + j) by A56, A67
.= (vs1 ^' vs2) . ((len vs1) + j) by A1
.= vs2 . k by A66, A67, A71, FINSEQ_6:141 ; :: thesis: verum

end;

end;

end;

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

end;

then cc is oriented by GRAPH_1:def 15;
hence c1 ^ c2 is oriented Chain of G ; :: thesis: verum

end;