let i be Nat; :: thesis: for G being Graph
for pe being FinSequence of the carrier' of G st 1 <= i & i <= len pe holds
( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G )
let G be Graph; :: thesis: for pe being FinSequence of the carrier' of G st 1 <= i & i <= len pe holds
( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G )
let pe be FinSequence of the carrier' of G; :: thesis: ( 1 <= i & i <= len pe implies ( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G ) )
assume ( 1 <= i & i <= len pe ) ; :: thesis: ( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G )
then i in dom pe by FINSEQ_3:25;
hence ( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G ) by GRAPH_5:8; :: thesis: verum