:: deftheorem Def11 defines DIJK:CompSeq GLIB_004:def 11 :
for G being real-weighted WGraph
for src being Vertex of G
for b₃ being DIJK:LabelingSeq of G holds
( b₃ = DIJK:CompSeq src iff ( b₃ . 0 = DIJK:Init src & ( for n being Nat holds b₃ . (n + 1) = DIJK:Step (b₃ . n) ) ) );