theorem Th46: :: GRAPH_5:48

for i being Nat
for W being Function
for G being Graph
for pe, qe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds
ex j being Nat st
( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )