let G be finite natural-weighted WGraph; :: thesis:
let EL be FF:ELabeling of G; :: thesis:
let source, sink be set ; :: thesis:
assume that
A1: EL has_valid_flow_from source,sink and
A2: for P being Path of G holds
( not P is_Walk_from source,sink or not P is_augmenting_wrt EL ) ; :: thesis:
reconsider src = source as Vertex of G by A1, Def2;
set CS = AP:CompSeq EL,src;
set Gn = AP:FindAugPath EL,src;
set Gn1 = (AP:CompSeq EL,src) . (((AP:CompSeq EL,src) .Lifespan() ) + 1);
reconsider V = dom (AP:FindAugPath EL,src) as Subset of (the_Vertices_of G) ;
set E1 = G .edgesDBetween V,((the_Vertices_of G) \ V);
set A1 = EL | (G .edgesDBetween V,((the_Vertices_of G) \ V));
set B1 = (the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V));
set e = choose (AP:NextBestEdges (AP:FindAugPath EL,src));
AP:CompSeq EL,src is halting by Th6;
then A3: (AP:CompSeq EL,src) . (((AP:CompSeq EL,src) .Lifespan() ) + 1) = AP:FindAugPath EL,src by GLIB_000:def 57;
A4: (AP:CompSeq EL,src) . (((AP:CompSeq EL,src) .Lifespan() ) + 1) = AP:Step (AP:FindAugPath EL,src) by Def12;

A5: now

assume A6: AP:NextBestEdges (AP:FindAugPath EL,src) <> {} ; :: thesis:

now

per cases by A6, Def9;

suppose A7: choose (AP:NextBestEdges (AP:FindAugPath EL,src)) is_forward_edge_wrt AP:FindAugPath EL,src ; :: thesis:

then (the_Source_of G) . (choose (AP:NextBestEdges (AP:FindAugPath EL,src))) in V by Def6;
then A8: AP:FindAugPath EL,src = (AP:FindAugPath EL,src) +* (((the_Target_of G) . (choose (AP:NextBestEdges (AP:FindAugPath EL,src)))) .--> (choose (AP:NextBestEdges (AP:FindAugPath EL,src)))) by A4, A3, A6, Def10;
not (the_Target_of G) . (choose (AP:NextBestEdges (AP:FindAugPath EL,src))) in V by A7, Def6;
hence contradiction by A8, Lm2; :: thesis:

end;

suppose choose (AP:NextBestEdges (AP:FindAugPath EL,src)) is_backward_edge_wrt AP:FindAugPath EL,src ; :: thesis:

then A9: not (the_Source_of G) . (choose (AP:NextBestEdges (AP:FindAugPath EL,src))) in V by Def7;
then AP:FindAugPath EL,src = (AP:FindAugPath EL,src) +* (((the_Source_of G) . (choose (AP:NextBestEdges (AP:FindAugPath EL,src)))) .--> (choose (AP:NextBestEdges (AP:FindAugPath EL,src)))) by A4, A3, A6, Def10;
hence contradiction by A9, Lm2; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

A10: now

set e = choose (AP:NextBestEdges (AP:FindAugPath EL,src));
let x be set ; :: thesis:
assume A11: x in G .edgesDBetween V,((the_Vertices_of G) \ V) ; :: thesis:
then A12: (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = EL . x by FUNCT_1:72;
A13: x DSJoins V,(the_Vertices_of G) \ V,G by A11, GLIB_000:def 33;
then (the_Target_of G) . x in (the_Vertices_of G) \ V by GLIB_000:def 18;
then A14: not (the_Target_of G) . x in V by XBOOLE_0:def 5;
A15: ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = (the_Weight_of G) . x by A11, FUNCT_1:72;
A16: (the_Source_of G) . x in V by A13, GLIB_000:def 18;

A17: now

assume (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x < ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x ; :: thesis:
then x is_forward_edge_wrt AP:FindAugPath EL,src by A11, A12, A15, A16, A14, Def6;
hence contradiction by A5, Def9; :: thesis:

end;

(EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x <= ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x by A1, A11, A12, A15, Def2;
hence (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x = ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) . x by A17, XXREAL_0:1; :: thesis:

end;

set E2 = G .edgesDBetween ((the_Vertices_of G) \ V),V;
set A2 = EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V);
set B2 = EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V);

now

set e = choose (AP:NextBestEdges (AP:FindAugPath EL,src));
let x be set ; :: thesis:
assume A18: x in G .edgesDBetween ((the_Vertices_of G) \ V),V ; :: thesis:
then A19: x DSJoins (the_Vertices_of G) \ V,V,G by GLIB_000:def 33;
then A20: (the_Target_of G) . x in V by GLIB_000:def 18;
(the_Source_of G) . x in (the_Vertices_of G) \ V by A19, GLIB_000:def 18;
then A21: not (the_Source_of G) . x in V by XBOOLE_0:def 5;
A22: (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = EL . x by A18, FUNCT_1:72;

A23: now

assume 0 < (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x ; :: thesis:
then x is_backward_edge_wrt AP:FindAugPath EL,src by A18, A22, A20, A21, Def7;
hence contradiction by A5, Def9; :: thesis:

end;

EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V) = (G .edgesDBetween ((the_Vertices_of G) \ V),V) --> 0 by PRE_POLY:def 13;
then (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = 0 by A18, FUNCOP_1:13;
hence (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x = (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) . x by A23; :: thesis:

end;

then Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) = Sum (EmptyBag (G .edgesDBetween ((the_Vertices_of G) \ V),V)) by GLIB_004:6;
then A24: Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)) = 0 by UPROOTS:13;
A25: not sink in dom (AP:FindAugPath EL,src) by A2, Th9;
then EL .flow source,sink = (Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) by A1, Th10, Th11;
then EL .flow source,sink = Sum ((the_Weight_of G) | (G .edgesDBetween V,((the_Vertices_of G) \ V))) by A10, A24, GLIB_004:6;
then for X being FF:ELabeling of G st X has_valid_flow_from source,sink holds
X .flow source,sink <= EL .flow source,sink by A25, Th10, Th12;
hence EL has_maximum_flow_from source,sink by A1, Def4; :: thesis: