:: deftheorem Def15 defines .flowSeq GLIB_005:def 15 :
for G being natural-weighted WGraph
for EL being FF:ELabeling of G
for W being Walk of G st W is_augmenting_wrt EL holds
for b₄ being FinSequence of NAT holds
( b₄ = W .flowSeq EL iff ( dom b₄ = dom (W .edgeSeq()) & ( for n being Nat st n in dom b₄ holds
( ( W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b₄ . n = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) ) & ( not W . (2 * n) DJoins W . ((2 * n) - 1),W . ((2 * n) + 1),G implies b₄ . n = EL . (W . (2 * n)) ) ) ) ) );