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) )
set FS = the Source of G;
set FT = the Target of G;
assume A1: len pe = 1 ; :: thesis: vertices pe = vertices (pe /. 1)
then A2: 1 in dom pe by FINSEQ_3:25;

now :: thesis: for x being object holds
( ( x in vertices pe implies x in vertices (pe /. 1) ) & ( x in vertices (pe /. 1) implies x in vertices pe ) )

let x be object ; :: 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 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: verum

end;

assume A7: 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: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: verum

end;

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