let G be Graph; :: thesis:
let pe be FinSequence of the carrier' of G; :: thesis:
set FS = the Source of G;
set FT = the Target of G;
assume A1: len pe = 1 ; :: thesis:
then A2: 1 in dom pe by FINSEQ_3:25;

assume x in vertices pe ; :: thesis:
then consider y being Vertex of G such that
A3: y = x and
A4: ex i being Nat st
( i in dom pe & y in vertices (pe /. i) ) ;
consider i being Nat such that
A5: i in dom pe and
A6: y in vertices (pe /. i) by A4;
( 1 <= i & i <= len pe ) by A5, FINSEQ_3:25;
hence x in vertices (pe /. 1) by A1, A3, A6, XXREAL_0:1; :: thesis:

end;

assume A7: x in vertices (pe /. 1) ; :: thesis:
then ( x = the Source of G . (pe /. 1) or x = the Target of G . (pe /. 1) ) by TARSKI:def 2;
then ( x = the Source of G . (pe . 1) or x = the Target of G . (pe . 1) ) by A1, FINSEQ_4:15;
then reconsider y = x as Vertex of G by A2, FINSEQ_2:11, FUNCT_2:5;
y in { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) ) } by A2, A7;
hence x in vertices pe ; :: thesis:

end;