let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G st len pe = 1 holds
vertices pe = vertices (pe /. 1)
let pe be FinSequence of the carrier' of G; :: thesis: ( len pe = 1 implies vertices pe = vertices (pe /. 1) )
assume A1: len pe = 1 ; :: thesis: vertices pe = vertices (pe /. 1)
set FS = the Source of G;
set FT = the Target of G;
A2: 1 in dom pe by A1, FINSEQ_3:27;

now

let x be set ; :: thesis: ( ( x in vertices pe implies x in vertices (pe /. 1) ) & ( x in vertices (pe /. 1) implies x in vertices pe ) )

hereby :: thesis: ( x in vertices (pe /. 1) implies x in vertices pe )

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

end;

assume A5: x in vertices (pe /. 1) ; :: thesis: x in vertices pe
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:24;
then reconsider y = x as Vertex of G by A2, FINSEQ_2:13, FUNCT_2:7;
y in { v where v is Vertex of G : ex i being Element of NAT st
( i in dom pe & v in vertices (pe /. i) ) } by A2, A5;
hence x in vertices pe ; :: thesis: verum

end;

hence vertices pe = vertices (pe /. 1) by TARSKI:2; :: thesis: verum