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 A1: ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 ) ; :: thesis: c1 ^ c2 is oriented Chain of G
then A2: ( vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 ) by Th5;
A3: ( len vs1 = (len c1) + 1 & len vs2 = (len c2) + 1 ) by A1, Def5;
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 A2, GRAPH_2:46;
for n being Element of 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 Element of 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 A4: ( 1 <= n & n < len (c1 ^ c2) ) ; :: thesis: the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n)
then A5: n in dom (c1 ^ c2) by FINSEQ_3:27;
A6: n + 1 <= len (c1 ^ c2) by A4, NAT_1:13;
A7: 1 < n + 1 by A4, NAT_1:13;

now

per cases ( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ) by A5, FINSEQ_1:38;

case A8: n in dom c1 ; :: thesis: ex v1, v2 being Element of the carrier of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 )

then A9: (c1 ^ c2) . n = c1 . n by FINSEQ_1:def 7;
set v1 = vs1 /. n;
set v2 = vs1 /. (n + 1);
A10: ( 1 <= n & n <= len c1 ) by A8, FINSEQ_3:27;
then A11: c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A1, Def5;
A12: n <= len vs1 by A3, A10, NAT_1:12;
( 1 <= n + 1 & n + 1 <= (len c1) + 1 ) by A10, NAT_1:12, XREAL_1:8;
then A13: ( 1 <= n + 1 & n + 1 <= len vs1 ) by A1, Def5;
then A14: ( vs1 /. n = vs1 . n & vs1 /. (n + 1) = vs1 . (n + 1) ) by A10, A12, FINSEQ_4:24;
( (vs1 ^' vs2) . n = vs1 . n & (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) ) by A10, A12, A13, GRAPH_2:14;
hence ex v1, v2 being Element of the carrier of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) by A9, A11, A14; :: thesis: verum

end;

case ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; :: thesis: ex v1, v2 being Element of the carrier 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
A15: ( k in dom c2 & n = (len c1) + k ) ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A16: (c1 ^ c2) . n = c2 . k by A15, FINSEQ_1:def 7;
A17: ( 1 <= k & k <= len c2 ) by A15, FINSEQ_3:27;
then A18: ( 1 <= k + 1 & k <= len vs2 & k + 1 <= len vs2 ) by A3, NAT_1:12, XREAL_1:9;
set v1 = vs2 /. k;
set v2 = vs2 /. (k + 1);
A19: ( vs2 /. k = vs2 . k & vs2 /. (k + 1) = vs2 . (k + 1) ) by A17, A18, FINSEQ_4:24;
A20: c2 . k orientedly_joins vs2 /. k,vs2 /. (k + 1) by A1, A17, Def5;
A21: k <= len vs2 by A3, A17, NAT_1:12;
0 + 1 <= k by A15, FINSEQ_3:27;
then consider j being Element of NAT such that
A22: ( 0 <= j & j < len vs2 & k = j + 1 ) by A21, GRAPH_2:1;
A23: (vs1 ^' vs2) . n = vs2 . k

proof

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

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

A25: 0 + 1 <= len vs1 by A3, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (len vs1) by A1, A15, A24, Def5
.= vs2 . k by A1, A24, A25, GRAPH_2:14 ; :: thesis: verum

end;

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

then A26: 1 <= j by A22, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (((len c1) + 1) + j) by A15, A22
.= (vs1 ^' vs2) . ((len vs1) + j) by A1, Def5
.= vs2 . k by A22, A26, GRAPH_2:15 ; :: thesis: verum

end;

end;

end;

A27: k < len vs2 by A3, A17, NAT_1:13;
(vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A15
.= (vs1 ^' vs2) . ((len vs1) + k) by A1, Def5
.= vs2 . (k + 1) by A17, A27, GRAPH_2:15 ;
hence ex v1, v2 being Element of the carrier of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) by A16, A19, A20, A23; :: thesis: verum

end;

end;

end;

then consider v1, v2 being Element of the carrier of G such that
A28: ( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) ;
A29: n + 1 in dom (c1 ^ c2) by A6, A7, FINSEQ_3:27;

now

per cases ( n + 1 in dom c1 or ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) ) by A29, FINSEQ_1:38;

case A30: n + 1 in dom c1 ; :: thesis: ex v2'', v3' being Element of the carrier of G st
( v2'' = (vs1 ^' vs2) . (n + 1) & v3' = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v2'',v3' )

then A31: (c1 ^ c2) . (n + 1) = c1 . (n + 1) by FINSEQ_1:def 7;
set v2' = vs1 /. (n + 1);
set v3 = vs1 /. ((n + 1) + 1);
A32: ( 1 <= n + 1 & n + 1 <= len c1 ) by A30, FINSEQ_3:27;
then A33: c1 . (n + 1) orientedly_joins vs1 /. (n + 1),vs1 /. ((n + 1) + 1) by A1, Def5;
A34: n + 1 <= len vs1 by A3, A32, NAT_1:12;
( 1 <= (n + 1) + 1 & (n + 1) + 1 <= (len c1) + 1 ) by A32, NAT_1:12, XREAL_1:8;
then A35: ( 1 <= (n + 1) + 1 & (n + 1) + 1 <= len vs1 ) by A1, Def5;
then A36: ( vs1 /. (n + 1) = vs1 . (n + 1) & vs1 /. ((n + 1) + 1) = vs1 . ((n + 1) + 1) ) by A32, A34, FINSEQ_4:24;
( (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) & (vs1 ^' vs2) . ((n + 1) + 1) = vs1 . ((n + 1) + 1) ) by A32, A34, A35, GRAPH_2:14;
hence ex v2'', v3' being Element of the carrier of G st
( v2'' = (vs1 ^' vs2) . (n + 1) & v3' = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v2'',v3' ) by A31, A33, A36; :: thesis: verum

end;

case ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) ; :: thesis: ex v2'', v3' being Element of the carrier of G st
( v2'' = (vs1 ^' vs2) . (n + 1) & v3' = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v2'',v3' )

then consider k being Nat such that
A37: ( k in dom c2 & n + 1 = (len c1) + k ) ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A38: (c1 ^ c2) . (n + 1) = c2 . k by A37, FINSEQ_1:def 7;
A39: ( 1 <= k & k <= len c2 ) by A37, FINSEQ_3:27;
then A40: ( 1 <= k + 1 & k <= len vs2 & k + 1 <= len vs2 ) by A3, NAT_1:12, XREAL_1:9;
set v2' = vs2 /. k;
set v3 = vs2 /. (k + 1);
A41: ( vs2 /. k = vs2 . k & vs2 /. (k + 1) = vs2 . (k + 1) ) by A39, A40, FINSEQ_4:24;
A42: c2 . k orientedly_joins vs2 /. k,vs2 /. (k + 1) by A1, A39, Def5;
A43: k <= len vs2 by A3, A39, NAT_1:12;
0 + 1 <= k by A37, FINSEQ_3:27;
then consider j being Element of NAT such that
A44: ( 0 <= j & j < len vs2 & k = j + 1 ) by A43, GRAPH_2:1;
A45: (vs1 ^' vs2) . (n + 1) = vs2 . k

proof

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

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

A47: 0 + 1 <= len vs1 by A3, NAT_1:13;
thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (len vs1) by A1, A37, A46, Def5
.= vs2 . k by A1, A46, A47, GRAPH_2:14 ; :: thesis: verum

end;

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

then A48: 1 <= j by A44, NAT_1:13;
thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + j) by A37, A44
.= (vs1 ^' vs2) . ((len vs1) + j) by A1, Def5
.= vs2 . k by A44, A48, GRAPH_2:15 ; :: thesis: verum

end;

end;

end;

A49: k < len vs2 by A3, A39, NAT_1:13;
(vs1 ^' vs2) . ((n + 1) + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A37
.= (vs1 ^' vs2) . ((len vs1) + k) by A1, Def5
.= vs2 . (k + 1) by A39, A49, GRAPH_2:15 ;
hence ex v2'', v3' being Element of the carrier of G st
( v2'' = (vs1 ^' vs2) . (n + 1) & v3' = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v2'',v3' ) by A38, A41, A42, A45; :: thesis: verum

end;

end;

end;

then consider v2', v3 being Element of the carrier of G such that
A50: ( v2' = (vs1 ^' vs2) . (n + 1) & v3 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v2',v3 ) ;
( the Source of G . ((c1 ^ c2) . n) = v1 & the Target of G . ((c1 ^ c2) . n) = v2 ) by A28, Def1;
hence the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) by A28, A50, Def1; :: thesis: verum

end;

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

end;