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;
assume A1: len pe = 1 ; :: thesis: pe is oriented Simple Chain of G
then A2: 1 in dom pe by FINSEQ_3:27;
set v1 = the Source of G . (pe . 1);
set v2 = the Target of G . (pe . 1);
reconsider v1 = the Source of G . (pe . 1), v2 = the Target of G . (pe . 1) as Element of the carrier of G by A2, FINSEQ_2:13, FUNCT_2:7;
set vs = <*v1,v2*>;
A3: len <*v1,v2*> = 2 by FINSEQ_1:61;
A4: len <*v1,v2*> = (len pe) + 1 by A1, FINSEQ_1:61;

now

let n be Element of 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 A5: n = 1 by A1, XXREAL_0:1;
( <*v1,v2*> /. 1 = v1 & <*v1,v2*> /. (1 + 1) = v2 ) by FINSEQ_4:26;
hence pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) by A5, GRAPH_4:def 1; :: thesis: verum

end;

then A6: <*v1,v2*> is_oriented_vertex_seq_of pe by A4, GRAPH_4:def 5;

A7: now

let n, m be Element of NAT ; :: thesis: ( 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m implies ( n = 1 & m = len <*v1,v2*> ) )
assume A8: ( 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m ) ; :: thesis: ( n = 1 & m = len <*v1,v2*> )
then n < 1 + 1 by A3, 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, XXREAL_0:2;
then 1 + 1 < m + 1 by XREAL_1:10;
then 2 <= m by NAT_1:13;
hence m = len <*v1,v2*> by A3, A8, XXREAL_0:1; :: thesis: verum

end;

A9: now

let n be Element of 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:27;
hence pe . n in the carrier' of G by FINSEQ_2:13; :: thesis: verum

end;

A10: now

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len <*v1,v2*> implies <*v1,v2*> . b₁ in the carrier of G )
assume A11: ( 1 <= n & 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 A11, XXREAL_0:1;
then <*v1,v2*> . n = v1 by FINSEQ_1:61;
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 A3, A11, XXREAL_0:1;
then <*v1,v2*> . n = v2 by FINSEQ_1:61;
hence <*v1,v2*> . n in the carrier of G ; :: thesis: verum

end;

end;

end;

A12: now

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len pe implies ex v1, v2 being Element of the carrier 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 the carrier of G st
( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 )
then A13: n = 1 by A1, XXREAL_0:1;
take v1 = v1; :: thesis: ex v2 being Element of the carrier 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 A13, FINSEQ_1:61; :: thesis: pe . n joins v1,v2
thus pe . n joins v1,v2 by A13, GRAPH_1:def 10; :: thesis: verum

end;

for n being Element of NAT st 1 <= n & n < len pe holds
not the Source of G . (pe . (n + 1)) <> the Target of G . (pe . n) by A1;
hence pe is oriented Simple Chain of G by A4, A6, A7, A9, A10, A12, GRAPH_1:def 12, GRAPH_1:def 13, GRAPH_4:def 7; :: thesis: verum