let i be Element of NAT ; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G
for v1 being Vertex of G st 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) holds
v1 in vertices pe
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G
for v1 being Vertex of G st 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) holds
v1 in vertices pe
let pe be FinSequence of the carrier' of G; :: thesis: for v1 being Vertex of G st 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) holds
v1 in vertices pe
let v1 be Vertex of G; :: thesis: ( 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) implies v1 in vertices pe )
assume A1: ( 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) ) ; :: thesis: v1 in vertices pe
then i in dom pe by FINSEQ_3:27;
hence v1 in vertices pe by A1, GRAPH_5:28; :: thesis: verum