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 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 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 Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) )

assume that

A1: IT is Simple and

A2: vs is_oriented_vertex_seq_of IT ; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

A3: len vs = (len IT) + 1 by A2, GRAPH_4:def 5;

consider vs9 being FinSequence of the carrier of G such that

A4: vs9 is_oriented_vertex_seq_of IT and

A5: for n, m being Nat st 1 <= n & n < m & m <= len vs9 & vs9 . n = vs9 . m holds

( n = 1 & m = len vs9 ) by A1, GRAPH_4:def 7;

A6: for n, m being Nat st 1 <= n & n < m & m <= len vs9 & vs9 . n = vs9 . m holds

( n = 1 & m = len vs9 ) by A5;

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 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 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 Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) )

assume that

A1: IT is Simple and

A2: vs is_oriented_vertex_seq_of IT ; :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

A3: len vs = (len IT) + 1 by A2, GRAPH_4:def 5;

consider vs9 being FinSequence of the carrier of G such that

A4: vs9 is_oriented_vertex_seq_of IT and

A5: for n, m being Nat st 1 <= n & n < m & m <= len vs9 & vs9 . n = vs9 . m holds

( n = 1 & m = len vs9 ) by A1, GRAPH_4:def 7;

A6: for n, m being Nat st 1 <= n & n < m & m <= len vs9 & vs9 . n = vs9 . m holds

( n = 1 & m = len vs9 ) by A5;

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

end;