let G be Graph; :: thesis: for e being set st e in the carrier' of G holds
for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>
let e be set ; :: thesis: ( e in the carrier' of G implies for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*> )
assume e in the carrier' of G ; :: thesis: for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>
then reconsider so = the Source of G . e, ta = the Target of G . e as Element of the carrier of G by FUNCT_2:5;
reconsider sota = <*so,ta*> as FinSequence of the carrier of G ;
let fe be directed Chain of G; :: thesis: ( fe = <*e*> implies vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*> )
assume A1: fe = <*e*> ; :: thesis: vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>
then A2: len fe = 1 by FINSEQ_1:39;
A3: sota is_vertex_seq_of fe

proof

thus len sota = (len fe) + 1 by A2, FINSEQ_1:44; :: according to GRAPH_2:def 2 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len fe or fe . b₁ joins sota /. b₁,sota /. (b₁ + 1) )
let n be Nat; :: thesis: ( not 1 <= n or not n <= len fe or fe . n joins sota /. n,sota /. (n + 1) )
A4: sota /. 2 = ta by FINSEQ_4:17;
assume ( 1 <= n & n <= len fe ) ; :: thesis: fe . n joins sota /. n,sota /. (n + 1)
then A5: n = 1 by A2, XXREAL_0:1;
( e joins so,ta & sota /. 1 = so ) by FINSEQ_4:17;
hence fe . n joins sota /. n,sota /. (n + 1) by A1, A5, A4; :: thesis: verum

end;

e = fe . 1 by A1;
then sota . 1 = the Source of G . (fe . 1) ;
hence vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*> by A1, A3, GRAPH_2:def 10; :: thesis: verum