let G be _finite natural-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
for W being Walk of G st W is V5() & W is_augmenting_wrt EL holds
0 < W .tolerance EL
let EL be FF:ELabeling of G; :: thesis: for W being Walk of G st W is V5() & W is_augmenting_wrt EL holds
0 < W .tolerance EL
let W be Walk of G; :: thesis: ( W is V5() & W is_augmenting_wrt EL implies 0 < W .tolerance EL )
assume that
A1: W is V5() and
A2: W is_augmenting_wrt EL ; :: thesis: 0 < W .tolerance EL
set T = W .tolerance EL;
W .tolerance EL in rng (W .flowSeq EL) by A1, A2, Def16;
then consider n being Nat such that
A3: n in dom (W .flowSeq EL) and
A4: W .tolerance EL = (W .flowSeq EL) . n by FINSEQ_2:10;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
dom (W .flowSeq EL) = dom (W .edgeSeq()) by A2, Def15;
then A5: 2 * n in dom W by A3, GLIB_001:78;
then 1 <= 2 * n by FINSEQ_3:25;
then reconsider 2n1 = (2 * n) - 1 as odd Element of NAT by INT_1:5;
2 * n <= len W by A5, FINSEQ_3:25;
then A6: (2 * n) - 1 < (len W) - 0 by XREAL_1:15;
set v1 = W . 2n1;
set e = W . (2 * n);
set v2 = W . ((2 * n) + 1);
A7: ((2 * n) - 1) + 2 = (2 * n) + 1 ;
A8: ((2 * n) - 1) + 1 = 2 * n ;
now :: thesis: 0 < W .tolerance EL
per cases ( W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G or not W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G ) ;
suppose A9: W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G ; :: thesis: 0 < W .tolerance EL
then A10: W .tolerance EL = ((the_Weight_of G) . (W . (2 * n))) - (EL . (W . (2 * n))) by A2, A3, A4, Def15;
EL . (W . (2 * n)) < (the_Weight_of G) . (W . (2 * n)) by A2, A6, A8, A7, A9;
then (EL . (W . (2 * n))) - (EL . (W . (2 * n))) < W .tolerance EL by A10, XREAL_1:14;
hence 0 < W .tolerance EL ; :: thesis: verum
end;
suppose A11: not W . (2 * n) DJoins W . 2n1,W . ((2 * n) + 1),G ; :: thesis: 0 < W .tolerance EL
then W .tolerance EL = EL . (W . (2 * n)) by A2, A3, A4, Def15;
hence 0 < W .tolerance EL by A2, A6, A8, A7, A11; :: thesis: verum
end;
end;
end;
hence 0 < W .tolerance EL ; :: thesis: verum