:: deftheorem Def10 defines DIJK:LabelingSeq GLIB_004:def 10 :
for G being real-weighted WGraph
for b₂ being ManySortedSet of NAT holds
( b₂ is DIJK:LabelingSeq of G iff for n being Nat holds b₂ . n is DIJK:Labeling of G );