let G be Graph; :: thesis:
let pe be FinSequence of the carrier' of G; :: thesis:
set p = pe;
set v1 = the Source of G . (pe . 1);
set v2 = the Target of G . (pe . 1);

A1: now :: thesis:

let n be Nat; :: thesis:
assume ( 1 <= n & n <= len pe ) ; :: thesis:
then n in dom pe by FINSEQ_3:25;
hence pe . n in the carrier' of G by FINSEQ_2:11; :: thesis:

end;

assume A2: len pe = 1 ; :: thesis:
then 1 in dom pe by FINSEQ_3:25;
then reconsider v1 = the Source of G . (pe . 1), v2 = the Target of G . (pe . 1) as Element of G by FINSEQ_2:11, FUNCT_2:5;
set vs = <*v1,v2*>;
A3: len <*v1,v2*> = (len pe) + 1 by A2, FINSEQ_1:44;

A4: now :: thesis:

let n be Nat; :: thesis:
assume ( 1 <= n & n <= len pe ) ; :: thesis:
then A5: n = 1 by A2, XXREAL_0:1;
take v1 = v1; :: thesis:
take v2 = v2; :: thesis:
thus ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) ) by A5, FINSEQ_1:44; :: thesis:
thus pe . n joins v1,v2 by A5, GRAPH_1:def 12; :: thesis:

end;

A6: len <*v1,v2*> = 2 by FINSEQ_1:44;

A7: now :: thesis:

let n, m be Nat; :: thesis:
assume that
A8: 1 <= n and
A9: n < m and
A10: m <= len <*v1,v2*> and
<*v1,v2*> . n = <*v1,v2*> . m ; :: thesis:
n < 1 + 1 by A6, A9, A10, XXREAL_0:2;
then n <= 1 by NAT_1:13;
hence n = 1 by A8, XXREAL_0:1; :: thesis:
1 < m by A8, A9, XXREAL_0:2;
then 1 + 1 < m + 1 by XREAL_1:8;
then 2 <= m by NAT_1:13;
hence m = len <*v1,v2*> by A6, A10, XXREAL_0:1; :: thesis:

end;

A11: now :: thesis:

let n be Nat; :: thesis:
assume that
A12: 1 <= n and
A13: n <= len <*v1,v2*> ; :: thesis:

per cases ;

suppose n < 1 + 1 ; :: thesis:

then n <= 1 by NAT_1:13;
then n = 1 by A12, XXREAL_0:1;
then <*v1,v2*> . n = v1 by FINSEQ_1:44;
hence <*v1,v2*> . n in the carrier of G ; :: thesis:

end;

suppose n >= 2 ; :: thesis:

then n = 2 by A6, A13, XXREAL_0:1;
then <*v1,v2*> . n = v2 by FINSEQ_1:44;
hence <*v1,v2*> . n in the carrier of G ; :: thesis:

end;

end;

end;

A14: for n being Nat st 1 <= n & n < len pe holds
not the Source of G . (pe . (n + 1)) <> the Target of G . (pe . n) by A2;

now :: thesis:

let n be Nat; :: thesis:
assume ( 1 <= n & n <= len pe ) ; :: thesis:
then A15: n = 1 by A2, XXREAL_0:1;
( <*v1,v2*> /. 1 = v1 & <*v1,v2*> /. (1 + 1) = v2 ) by FINSEQ_4:17;
hence pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) by A15, GRAPH_4:def 1; :: thesis:

end;

then <*v1,v2*> is_oriented_vertex_seq_of pe by A3, GRAPH_4:def 5;
hence pe is oriented Simple Chain of G by A3, A7, A1, A11, A4, A14, GRAPH_1:def 14, GRAPH_1:def 15, GRAPH_4:def 7; :: thesis: