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