let G be Graph; :: thesis: for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds
p ^ q is oriented Chain of G
let p, q be oriented Chain of G; :: thesis: ( the Target of G . (p . (len p)) = the Source of G . (q . 1) implies p ^ q is oriented Chain of G )
assume A1: the Target of G . (p . (len p)) = the Source of G . (q . 1) ; :: thesis: p ^ q is oriented Chain of G

per cases ( p = {} or q = {} or ( not p = {} & not q = {} ) ) ;

suppose A2: ( p = {} or q = {} ) ; :: thesis: p ^ q is oriented Chain of G

hereby :: thesis: verum

per cases ( p = {} or q = {} ) by A2;

suppose p = {} ; :: thesis: p ^ q is oriented Chain of G

hence p ^ q is oriented Chain of G by FINSEQ_1:47; :: thesis: verum

end;

suppose q = {} ; :: thesis: p ^ q is oriented Chain of G

hence p ^ q is oriented Chain of G by FINSEQ_1:47; :: thesis: verum

end;

end;

end;

end;

suppose ( not p = {} & not q = {} ) ; :: thesis: p ^ q is oriented Chain of G

then A3: ( len p >= 1 & len q >= 1 ) by FINSEQ_1:28;
consider vs1 being FinSequence of the carrier of G such that
A4: vs1 is_oriented_vertex_seq_of p by GRAPH_4:10;
consider vs2 being FinSequence of the carrier of G such that
A5: vs2 is_oriented_vertex_seq_of q by GRAPH_4:10;
A6: ( len vs1 = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len p holds
p . n orientedly_joins vs1 /. n,vs1 /. (n + 1) ) ) by A4, GRAPH_4:def 5;
then A7: len vs1 >= 1 by NAT_1:12;
p . (len p) orientedly_joins vs1 /. (len p),vs1 /. ((len p) + 1) by A3, A4, GRAPH_4:def 5;
then A8: the Target of G . (p . (len p)) = vs1 /. (len vs1) by A6, GRAPH_4:def 1
.= vs1 . (len vs1) by A7, FINSEQ_4:24 ;
( len vs2 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len q holds
q . n orientedly_joins vs2 /. n,vs2 /. (n + 1) ) ) by A5, GRAPH_4:def 5;
then A9: len vs2 >= 1 by NAT_1:12;
q . 1 orientedly_joins vs2 /. 1,vs2 /. (1 + 1) by A3, A5, GRAPH_4:def 5;
then the Source of G . (q . 1) = vs2 /. 1 by GRAPH_4:def 1
.= vs2 . 1 by A9, FINSEQ_4:24 ;
hence p ^ q is oriented Chain of G by A1, A4, A5, A8, GRAPH_4:15; :: thesis: verum

end;

end;