:: deftheorem Def12 defines AP:CompSeq GLIB_005:def 12 :
for G being real-weighted WGraph
for EL being FF:ELabeling of G
for source being Vertex of G
for b₄ being AP:VLabelingSeq of EL holds
( b₄ = AP:CompSeq (EL,source) iff ( b₄ . 0 = source .--> 1 & ( for n being Nat holds b₄ . (n + 1) = AP:Step (b₄ . n) ) ) );