let i be 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 that
A1: ( 1 <= i & i <= len pe ) and
A2: ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) ; :: thesis: v1 in vertices pe
i in dom pe by A1, FINSEQ_3:25;
hence v1 in vertices pe by A2, GRAPH_5:24; :: thesis: verum