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