theorem :: GRAPH_5:8

for i being Nat
for G being Graph
for pe being FinSequence of the carrier' of G st i in dom pe holds
( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G ) by FINSEQ_2:11, FUNCT_2:5;