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 vs = <*t,s*>;
set c = <*e*>;
A2: len <*e*> = 1 by FINSEQ_1:56;
hence len <*t,s*> = (len <*e*>) + 1 by FINSEQ_1:61; :: according to GRAPH_2:def 7 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not b₁ <= len <*e*> or <*e*> . b₁ joins <*t,s*> /. b₁,<*t,s*> /. (b₁ + 1) )
let n be Element of 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 A3: n = 1 by A2, XXREAL_0:1;
( <*e*> . 1 = e & <*t,s*> . 1 = t & <*t,s*> . (1 + 1) = s & <*t,s*> /. 1 = t & <*t,s*> /. (1 + 1) = s ) by FINSEQ_1:57, FINSEQ_1:61, FINSEQ_4:26;
hence <*e*> . n joins <*t,s*> /. n,<*t,s*> /. (n + 1) by A1, A3, GRAPH_1:def 10; :: thesis: verum