let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut m,n is_augmenting_wrt EL
let EL be FF:ELabeling of ; :: thesis: for W being Walk of G
for m, n being Nat st W is_augmenting_wrt EL holds
W .cut m,n is_augmenting_wrt EL
let W be Walk of G; :: thesis: for m, n being Nat st W is_augmenting_wrt EL holds
W .cut m,n is_augmenting_wrt EL
let m, n be Nat; :: thesis: ( W is_augmenting_wrt EL implies W .cut m,n is_augmenting_wrt EL )
assume AA: W is_augmenting_wrt EL ; :: thesis: W .cut m,n is_augmenting_wrt EL
set W2 = W .cut m,n;

now

per cases ( ( not m is even & not n is even & m <= n & n <= len W ) or m is even or n is even or not m <= n or not n <= len W ) ;

suppose A1: ( not m is even & not n is even & m <= n & n <= len W ) ; :: thesis: W .cut m,n is_augmenting_wrt EL

then reconsider m' = m, n' = n as odd Element of NAT by ORDINAL1:def 13;

now

let x be odd Nat; :: thesis: ( x < len (W .cut m,n) implies ( ( (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G implies EL . ((W .cut m,n) . (x + 1)) < (the_Weight_of G) . ((W .cut m,n) . (x + 1)) ) & ( not (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G implies 0 < EL . ((W .cut m,n) . (x + 1)) ) ) )
reconsider x' = x as Element of NAT by ORDINAL1:def 13;
assume x < len (W .cut m,n) ; :: thesis: ( ( (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G implies EL . ((W .cut m,n) . (x + 1)) < (the_Weight_of G) . ((W .cut m,n) . (x + 1)) ) & ( not (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G implies 0 < EL . ((W .cut m,n) . (x + 1)) ) )
then A2: ( x' in dom (W .cut m,n) & x' + 1 in dom (W .cut m,n) & x' + 2 in dom (W .cut m,n) ) by GLIB_001:13;
set v1b = (W .cut m,n) . x;
set eb = (W .cut m,n) . (x + 1);
set v2b = (W .cut m,n) . (x + 2);
( m' <= n' & n' <= len W ) by A1;
then A3: ( (W .cut m,n) . x' = W . ((m' + x') - 1) & (m' + x') - 1 in dom W & (W .cut m,n) . (x' + 1) = W . ((m' + (x' + 1)) - 1) & (m' + (x' + 1)) - 1 in dom W & (W .cut m,n) . (x' + 2) = W . ((m' + (x' + 2)) - 1) & (m' + (x' + 2)) - 1 in dom W ) by A2, GLIB_001:48;
then reconsider a = (m' + x) - 1, a1 = (m + (x + 1)) - 1, a2 = (m + (x + 2)) - 1 as Element of NAT ;
reconsider a = a as odd Element of NAT ;
set v1a = W . a;
set ea = W . (a + 1);
set v2a = W . (a + 2);
a2 <= len W by A3, FINSEQ_3:27;
then A4: ((m + (x + 2)) - 1) - 2 < (len W) - 0 by XREAL_1:17;

hereby :: thesis: ( not (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G implies 0 < EL . ((W .cut m,n) . (x + 1)) )

assume (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G ; :: thesis: EL . ((W .cut m,n) . (x + 1)) < (the_Weight_of G) . ((W .cut m,n) . (x + 1))
then W . (a + 1) DJoins W . a,W . (a + 2),G by A3;
hence EL . ((W .cut m,n) . (x + 1)) < (the_Weight_of G) . ((W .cut m,n) . (x + 1)) by AA, A3, A4, Def12; :: thesis: verum

end;

assume not (W .cut m,n) . (x + 1) DJoins (W .cut m,n) . x,(W .cut m,n) . (x + 2),G ; :: thesis: 0 < EL . ((W .cut m,n) . (x + 1))
then not W . (a + 1) DJoins W . a,W . (a + 2),G by A3;
hence 0 < EL . ((W .cut m,n) . (x + 1)) by AA, A3, A4, Def12; :: thesis: verum

end;

hence W .cut m,n is_augmenting_wrt EL by Def12; :: thesis: verum

end;

suppose ( m is even or n is even or not m <= n or not n <= len W ) ; :: thesis: W .cut m,n is_augmenting_wrt EL

hence W .cut m,n is_augmenting_wrt EL by AA, GLIB_001:def 11; :: thesis: verum

end;

end;

end;

hence W .cut m,n is_augmenting_wrt EL ; :: thesis: verum