:: deftheorem Def17 defines PRIM:CompSeq GLIB_004:def 17 :
for G being real-weighted WGraph
for b₂ being PRIM:LabelingSeq of G holds
( b₂ = PRIM:CompSeq G iff ( b₂ . 0 = PRIM:Init G & ( for n being Nat holds b₂ . (n + 1) = PRIM:Step (b₂ . n) ) ) );