theorem Th4: :: GLIB_005:4

for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G holds dom ((AP:CompSeq (EL,source)) . 0) = {source}