let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G st len pe = 1 holds
pe is oriented Simple Chain of G
let pe be FinSequence of the carrier' of G; :: thesis: ( len pe = 1 implies pe is oriented Simple Chain of G )
set p = pe;
set v1 = the Source of G . (pe . 1);
set v2 = the Target of G . (pe . 1);

A1: now :: thesis: for n being Nat st 1 <= n & n <= len pe holds
pe . n in the carrier' of G

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

end;

assume A2: len pe = 1 ; :: thesis: pe is oriented Simple Chain of G
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: for n being Nat st 1 <= n & n <= len pe holds
ex v1, v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )

let n be Nat; :: thesis: ( 1 <= n & n <= len pe implies ex v1, v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 ) )
assume ( 1 <= n & n <= len pe ) ; :: thesis: ex v1, v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )
then A5: n = 1 by A2, XXREAL_0:1;
take v1 = v1; :: thesis: ex v2 being Element of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )
take v2 = v2; :: thesis: ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )
thus ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) ) by A5; :: thesis: pe . n joins v1,v2
thus pe . n joins v1,v2 by A5, GRAPH_1:def 12; :: thesis: verum

end;

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

A7: now :: thesis: for n, m being Nat st 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m holds
( n = 1 & m = len <*v1,v2*> )

let n, m be Nat; :: thesis: ( 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m implies ( n = 1 & m = len <*v1,v2*> ) )
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 & m = len <*v1,v2*> )
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: m = len <*v1,v2*>
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: verum

end;

A11: now :: thesis: for n being Nat st 1 <= n & n <= len <*v1,v2*> holds
<*v1,v2*> . n in the carrier of G

let n be Nat; :: thesis: ( 1 <= n & n <= len <*v1,v2*> implies <*v1,v2*> . b₁ in the carrier of G )
assume that
A12: 1 <= n and
A13: n <= len <*v1,v2*> ; :: thesis: <*v1,v2*> . b₁ in the carrier of G

per cases ( n < 1 + 1 or n >= 2 ) ;

suppose n < 1 + 1 ; :: thesis: <*v1,v2*> . b₁ in the carrier of G

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

end;

suppose n >= 2 ; :: thesis: <*v1,v2*> . b₁ in the carrier of G

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

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: for n being Nat st 1 <= n & n <= len pe holds
pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1)

let n be Nat; :: thesis: ( 1 <= n & n <= len pe implies pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) )
assume ( 1 <= n & n <= len pe ) ; :: thesis: pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1)
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: verum

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: verum