let G be Graph; :: thesis: for IT being oriented Chain of G
for vs being FinSequence of the carrier of G st IT is Simple & vs is_oriented_vertex_seq_of IT holds
for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )
let IT be oriented Chain of G; :: thesis: for vs being FinSequence of the carrier of G st IT is Simple & vs is_oriented_vertex_seq_of IT holds
for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )
let vs be FinSequence of the carrier of G; :: thesis: ( IT is Simple & vs is_oriented_vertex_seq_of IT implies for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) )
assume A1: ( IT is Simple & vs is_oriented_vertex_seq_of IT ) ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )
then consider vs' being FinSequence of the carrier of G such that
A2: ( vs' is_oriented_vertex_seq_of IT & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs' & vs' . n = vs' . m holds
( n = 1 & m = len vs' ) ) ) by GRAPH_4:def 7;
A3: ( len vs = (len IT) + 1 & ( for n being Element of NAT st 1 <= n & n <= len IT holds
IT . n orientedly_joins vs /. n,vs /. (n + 1) ) ) by A1, GRAPH_4:def 5;

per cases ( IT <> {} or IT = {} ) ;

suppose IT <> {} ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

then vs = vs' by A1, A2, GRAPH_4:11;
hence for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by A2; :: thesis: verum

end;

suppose IT = {} ; :: thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

then len IT = 0 ;
hence for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) by A3, XXREAL_0:2; :: thesis: verum

end;

end;