theorem Th5: :: GLIB_005:5

for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G
for i, j being Nat st i <= j holds
dom ((AP:CompSeq (EL,source)) . i) c= dom ((AP:CompSeq (EL,source)) . j)