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

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