let G be Graph; :: thesis: for e being set
for s, t being Vertex of G st s = the Source of G . e & t = the Target of G . e holds
<*t,s*> is_vertex_seq_of <*e*>
let e be set ; :: thesis: for s, t being Vertex of G st s = the Source of G . e & t = the Target of G . e holds
<*t,s*> is_vertex_seq_of <*e*>
let s, t be Element of the carrier of G; :: thesis: ( s = the Source of G . e & t = the Target of G . e implies <*t,s*> is_vertex_seq_of <*e*> )
assume A1: ( s = the Source of G . e & t = the Target of G . e ) ; :: thesis: <*t,s*> is_vertex_seq_of <*e*>
set c = <*e*>;
set vs = <*t,s*>;
A2: <*t,s*> /. (1 + 1) = s by FINSEQ_4:17;
A3: len <*e*> = 1 by FINSEQ_1:39;
hence len <*t,s*> = (len <*e*>) + 1 by FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len <*e*> or <*e*> . b₁ joins <*t,s*> /. b₁,<*t,s*> /. (b₁ + 1) )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len <*e*> or <*e*> . n joins <*t,s*> /. n,<*t,s*> /. (n + 1) )
assume ( 1 <= n & n <= len <*e*> ) ; :: thesis: <*e*> . n joins <*t,s*> /. n,<*t,s*> /. (n + 1)
then A4: n = 1 by A3, XXREAL_0:1;
( <*e*> . 1 = e & <*t,s*> /. 1 = t ) by FINSEQ_4:17;
hence <*e*> . n joins <*t,s*> /. n,<*t,s*> /. (n + 1) by A1, A4, A2; :: thesis: verum