let G be Graph; 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 ; 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; ( 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 )
; <*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; GRAPH_2:def 2 for b1 being set holds
( not 1 <= b1 or not b1 <= len <*e*> or <*e*> . b1 joins <*t,s*> /. b1,<*t,s*> /. (b1 + 1) )
let n be Nat; ( 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*> )
; <*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_1:40, FINSEQ_4:17;
hence
<*e*> . n joins <*t,s*> /. n,<*t,s*> /. (n + 1)
by A1, A4, A2; verum