let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for W being Walk of G
for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
let EL be FF:ELabeling of ; :: thesis: for W being Walk of G
for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
let W be Walk of G; :: thesis: for e, v being set st W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) holds
W .addEdge e is_augmenting_wrt EL
let e, v be set ; :: thesis: ( W is_augmenting_wrt EL & not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) implies W .addEdge e is_augmenting_wrt EL )
assume AA: W is_augmenting_wrt EL ; :: thesis: ( v in W .vertices() or ( not ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) & not ( e DJoins v,W .last() ,G & 0 < EL . e ) ) or W .addEdge e is_augmenting_wrt EL )
set W2 = W .addEdge e;
assume A1: ( not v in W .vertices() & ( ( e DJoins W .last() ,v,G & EL . e < (the_Weight_of G) . e ) or ( e DJoins v,W .last() ,G & 0 < EL . e ) ) ) ; :: thesis: W .addEdge e is_augmenting_wrt EL
let n be odd Nat; :: according to GLIB_005:def 8 :: thesis: ( n < len (W .addEdge e) implies ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) ) )
assume A2: n < len (W .addEdge e) ; :: thesis: ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )
A3: e Joins W .last() ,v,G by A1, GLIB_000:19;

now

per cases ( n < len W or n >= len W ) ;

suppose A4: n < len W ; :: thesis: ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )

reconsider n' = n as Element of NAT by ORDINAL1:def 13;
( n' in dom W & n' + 1 in dom W & n' + 2 in dom W ) by A4, GLIB_001:13;
then ( W . n = (W .addEdge e) . n & W . (n + 1) = (W .addEdge e) . (n + 1) & W . (n + 2) = (W .addEdge e) . (n + 2) ) by A3, GLIB_001:66;
hence ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) ) by AA, A4, Def12; :: thesis: verum

end;

suppose A5: n >= len W ; :: thesis: ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) )

n + 1 <= len (W .addEdge e) by A2, NAT_1:13;
then n + 1 <= (len W) + (2 * 1) by A3, GLIB_001:65;
then n + 1 < ((len W) + 1) + 1 by XXREAL_0:1;
then n + 1 <= (len W) + 1 by NAT_1:13;
then n <= len W by XREAL_1:8;
then A6: ( 1 <= n & n = len W ) by A5, HEYTING3:1, XXREAL_0:1;
then n in dom W by FINSEQ_3:27;
then A7: (W .addEdge e) . n = W . n by A3, GLIB_001:66
.= W .last() by A6, GLIB_001:def 7 ;
A8: ( (W .addEdge e) . (n + 1) = e & (W .addEdge e) . (n + 2) = v ) by A3, A6, GLIB_001:66;

now

assume ( e DJoins W .last() ,v,G & e DJoins v,W .last() ,G ) ; :: thesis: contradiction
then ( (the_Source_of G) . e = W .last() & (the_Source_of G) . e = v ) by GLIB_000:def 16;
hence contradiction by A1, GLIB_001:89; :: thesis: verum

end;

hence ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) by A1, A7, A8; :: thesis: ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) )
assume not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G ; :: thesis: 0 < EL . ((W .addEdge e) . (n + 1))
hence 0 < EL . ((W .addEdge e) . (n + 1)) by A1, A7, A8; :: thesis: verum

end;

end;

end;

hence ( ( (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies EL . ((W .addEdge e) . (n + 1)) < (the_Weight_of G) . ((W .addEdge e) . (n + 1)) ) & ( not (W .addEdge e) . (n + 1) DJoins (W .addEdge e) . n,(W .addEdge e) . (n + 2),G implies 0 < EL . ((W .addEdge e) . (n + 1)) ) ) ; :: thesis: verum