:: deftheorem Def20 defines FF:CompSeq GLIB_005:def 20 :
for G being _finite natural-weighted WGraph
for source, sink being Vertex of G
for b₄ being FF:ELabelingSeq of G holds
( b₄ = FF:CompSeq (G,source,sink) iff ( b₄ . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds b₄ . (n + 1) = FF:Step ((b₄ . n),source,sink) ) ) );