let G be Graph; :: thesis: {} is oriented Simple Chain of G
set v = the Element of G;
set vs = <* the Element of G*>;

A1: now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len <* the Element of G*> & <* the Element of G*> . n = <* the Element of G*> . m holds
( n = 1 & m = len <* the Element of G*> )

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len <* the Element of G*> & <* the Element of G*> . n = <* the Element of G*> . m implies ( n = 1 & m = len <* the Element of G*> ) )
assume that
A2: ( 1 <= n & n < m & m <= len <* the Element of G*> ) and
<* the Element of G*> . n = <* the Element of G*> . m ; :: thesis: ( n = 1 & m = len <* the Element of G*> )
assume ( not n = 1 or not m = len <* the Element of G*> ) ; :: thesis: contradiction
len <* the Element of G*> = 1 by FINSEQ_1:39;
hence contradiction by A2, XXREAL_0:2; :: thesis: verum

end;

<* the Element of G*> is_oriented_vertex_seq_of {} by GRAPH_4:8;
hence {} is oriented Simple Chain of G by A1, GRAPH_1:14, GRAPH_4:def 7; :: thesis: verum