theorem Th7: :: GLIB_005:7

for G being finite real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq (EL,source)) . n) holds
((AP:CompSeq (EL,source)) . n) . v = (AP:FindAugPath (EL,source)) . v