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

end;

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

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

end;

end;

end;

end;

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

consider vs2 being FinSequence of the carrier of G such that
A4: vs2 is_oriented_vertex_seq_of q by GRAPH_4:9;
len vs2 = (len q) + 1 by A4, GRAPH_4:def 5;
then A5: len vs2 >= 1 by NAT_1:12;
len q >= 1 by A3, FINSEQ_1:20;
then q . 1 orientedly_joins vs2 /. 1,vs2 /. (1 + 1) by A4, GRAPH_4:def 5;
then A6: the Source of G . (q . 1) = vs2 /. 1 by GRAPH_4:def 1
.= vs2 . 1 by A5, FINSEQ_4:15 ;
consider vs1 being FinSequence of the carrier of G such that
A7: vs1 is_oriented_vertex_seq_of p by GRAPH_4:9;
A8: len vs1 = (len p) + 1 by A7, GRAPH_4:def 5;
then A9: len vs1 >= 1 by NAT_1:12;
len p >= 1 by A3, FINSEQ_1:20;
then p . (len p) orientedly_joins vs1 /. (len p),vs1 /. ((len p) + 1) by A7, GRAPH_4:def 5;
then the Target of G . (p . (len p)) = vs1 /. (len vs1) by A8, GRAPH_4:def 1
.= vs1 . (len vs1) by A9, FINSEQ_4:15 ;
hence p ^ q is oriented Chain of G by A1, A7, A4, A6, GRAPH_4:14; :: thesis: verum

end;

end;