let G be finite natural-weighted WGraph; :: thesis:
let EL be FF:ELabeling of G; :: thesis:
let source, sink be set ; :: thesis:
let P be Path of G; :: thesis:
assume that
A1: source <> sink and
A2: P is_Walk_from source,sink and
A3: P is_augmenting_wrt EL ; :: thesis:
A4: P .last() = sink by A2, GLIB_001:def 23;
P .first() = source by A2, GLIB_001:def 23;
then not P is trivial by A1, A4, GLIB_001:128;
then 3 <= len P by GLIB_001:126;
then reconsider lenP2g = (len P) - (2 * 1) as odd Element of NAT by INT_1:18, XXREAL_0:2;
set e1 = P . (lenP2g + 1);
set EI1 = EL | (G .edgesInto {sink});
set EO1 = EL | (G .edgesOutOf {sink});
set EL2 = FF:PushFlow EL,P;
set T = P .tolerance EL;
A5: P . (len P) = sink by A2, GLIB_001:18;
A6: lenP2g < (len P) - 0 by XREAL_1:17;
then A7: P . (lenP2g + 1) Joins P . lenP2g,P . (lenP2g + 2),G by GLIB_001:def 3;
then A8: P . (lenP2g + 1) in the_Edges_of G by GLIB_000:def 15;

now

per cases ;

suppose A9: P . (lenP2g + 1) DJoins P . lenP2g,P . (lenP2g + 2),G ; :: thesis:

then (the_Target_of G) . (P . (lenP2g + 1)) = P . (lenP2g + 2) by GLIB_000:def 16
.= sink by A2, GLIB_001:18 ;
then (the_Target_of G) . (P . (lenP2g + 1)) in {sink} by TARSKI:def 1;
then A10: P . (lenP2g + 1) in G .edgesInto {sink} by A8, GLIB_000:def 28;
set EI2 = (EL | (G .edgesInto {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL)));
A11: dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) = G .edgesInto {sink} by PARTFUN1:def 4;
A12: dom ((EL | (G .edgesInto {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL)))) = (dom (EL | (G .edgesInto {sink}))) \/ (dom ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL)))) by FUNCT_4:def 1
.= (dom (EL | (G .edgesInto {sink}))) \/ {(P . (lenP2g + 1))} by FUNCOP_1:19
.= (G .edgesInto {sink}) \/ {(P . (lenP2g + 1))} by PARTFUN1:def 4
.= G .edgesInto {sink} by A10, ZFMISC_1:46 ;
then reconsider EI2 = (EL | (G .edgesInto {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL))) as Rbag of G .edgesInto {sink} by PARTFUN1:def 4, RELAT_1:def 18;
A13: (FF:PushFlow EL,P) . (P . (lenP2g + 1)) = (EL . (P . (lenP2g + 1))) + (P .tolerance EL) by A3, A6, A9, Def17;

now

let e be set ; :: thesis:
assume A14: e in dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) ; :: thesis:
then A15: e in G .edgesInto {sink} by PARTFUN1:def 4;
A16: ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = (FF:PushFlow EL,P) . e by A11, A14, FUNCT_1:72;
(the_Target_of G) . e in {sink} by A15, GLIB_000:def 28;
then A17: (the_Target_of G) . e = sink by TARSKI:def 1;

now

per cases ;

suppose A18: e = P . (lenP2g + 1) ; :: thesis:

then e in {(P . (lenP2g + 1))} by TARSKI:def 1;
then e in dom ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL))) by FUNCOP_1:19;
then EI2 . e = ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL))) . (P . (lenP2g + 1)) by A18, FUNCT_4:14
.= ((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL) by FUNCOP_1:87
.= (FF:PushFlow EL,P) . (P . (lenP2g + 1)) by A13, A15, A18, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = EI2 . e by A11, A14, A18, FUNCT_1:72; :: thesis:

end;

suppose A19: e <> P . (lenP2g + 1) ; :: thesis:

A20: now

assume e in P .edges() ; :: thesis:
then consider v1, v2 being Vertex of G, m being odd Element of NAT such that
A21: m + 2 <= len P and
A22: v1 = P . m and
A23: e = P . (m + 1) and
A24: v2 = P . (m + 2) and
A25: e Joins v1,v2,G by GLIB_001:104;

now

per cases by A17, A25, GLIB_000:def 15;

suppose A26: v1 = sink ; :: thesis:

A27: (m + 2) - 2 < (len P) - 0 by A21, XREAL_1:17;
P . m = P . (len P) by A2, A22, A26, GLIB_001:18;
then m = 1 by A27, GLIB_001:def 28;
hence contradiction by A1, A2, A22, A26, GLIB_001:18; :: thesis:

end;

suppose v2 = sink ; :: thesis:

then A28: P . (m + 2) = P . (len P) by A2, A24, GLIB_001:18;

now

assume m + 2 < len P ; :: thesis:
then m + 2 = 1 by A28, GLIB_001:def 28;
then m = 1 - 2 ;
hence contradiction by ABIAN:12; :: thesis:

end;

then m + 2 = len P by A21, XXREAL_0:1;
hence contradiction by A19, A23; :: thesis:

end;

hence contradiction ; :: thesis:

end;

not e in {(P . (lenP2g + 1))} by A19, TARSKI:def 1;
then not e in dom ((P . (lenP2g + 1)) .--> (((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) + (P .tolerance EL))) by FUNCOP_1:19;
then EI2 . e = (EL | (G .edgesInto {sink})) . e by FUNCT_4:12
.= EL . e by A15, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = EI2 . e by A3, A15, A16, A20, Def17; :: thesis:

end;

hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = EI2 . e ; :: thesis:

end;

then A29: Sum ((FF:PushFlow EL,P) | (G .edgesInto {sink})) = ((Sum (EL | (G .edgesInto {sink}))) + ((P .tolerance EL) + ((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))))) - ((EL | (G .edgesInto {sink})) . (P . (lenP2g + 1))) by A12, A11, FUNCT_1:9, GLIB_004:9
.= (Sum (EL | (G .edgesInto {sink}))) + (P .tolerance EL) ;
A30: dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} by PARTFUN1:def 4;

A31: now

let e be set ; :: thesis:
assume A32: e in dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) ; :: thesis:
then A33: e in G .edgesOutOf {sink} by PARTFUN1:def 4;
then (the_Source_of G) . e in {sink} by GLIB_000:def 29;
then A34: (the_Source_of G) . e = sink by TARSKI:def 1;

now

assume e in P .edges() ; :: thesis:
then consider v1, v2 being Vertex of G, m being odd Element of NAT such that
A35: m + 2 <= len P and
A36: v1 = P . m and
A37: e = P . (m + 1) and
A38: v2 = P . (m + 2) and
A39: e Joins v1,v2,G by GLIB_001:104;

now

per cases by A34, A39, GLIB_000:def 15;

suppose A40: v1 = sink ; :: thesis:

A41: (m + 2) - 2 < (len P) - 0 by A35, XREAL_1:17;
P . m = P . (len P) by A2, A36, A40, GLIB_001:18;
then m = 1 by A41, GLIB_001:def 28;
hence contradiction by A1, A2, A36, A40, GLIB_001:18; :: thesis:

end;

suppose v2 = sink ; :: thesis:

then A42: P . (m + 2) = P . (len P) by A2, A38, GLIB_001:18;

now

assume m + 2 < len P ; :: thesis:
then m + 2 = 1 by A42, GLIB_001:def 28;
then 1 <= 1 - 2 by ABIAN:12;
hence contradiction ; :: thesis:

end;

then m + 2 = len P by A35, XXREAL_0:1;
then A43: P . lenP2g = sink by A9, A34, A37, GLIB_000:def 16;
then lenP2g = 1 by A6, A5, GLIB_001:def 28;
hence contradiction by A1, A2, A43, GLIB_001:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then (FF:PushFlow EL,P) . e = EL . e by A3, A33, Def17
.= (EL | (G .edgesOutOf {sink})) . e by A33, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = (EL | (G .edgesOutOf {sink})) . e by A30, A32, FUNCT_1:72; :: thesis:

end;

dom (EL | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} by PARTFUN1:def 4;
hence (FF:PushFlow EL,P) .flow source,sink = ((Sum (EL | (G .edgesInto {sink}))) + (P .tolerance EL)) - (Sum (EL | (G .edgesOutOf {sink}))) by A29, A30, A31, FUNCT_1:9
.= ((Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})))) + (P .tolerance EL)
.= (EL .flow source,sink) + (P .tolerance EL) ;
:: thesis:

end;

suppose A44: not P . (lenP2g + 1) DJoins P . lenP2g,P . (lenP2g + 2),G ; :: thesis:

then A45: P . (lenP2g + 1) DJoins P . (lenP2g + 2),P . lenP2g,G by A7, GLIB_000:19;
then (the_Source_of G) . (P . (lenP2g + 1)) = P . (lenP2g + 2) by GLIB_000:def 16
.= sink by A2, GLIB_001:18 ;
then (the_Source_of G) . (P . (lenP2g + 1)) in {sink} by TARSKI:def 1;
then A46: P . (lenP2g + 1) in G .edgesOutOf {sink} by A8, GLIB_000:def 29;
set EO2 = (EL | (G .edgesOutOf {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL)));
A47: dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} by PARTFUN1:def 4;
A48: dom ((EL | (G .edgesOutOf {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL)))) = (dom (EL | (G .edgesOutOf {sink}))) \/ (dom ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL)))) by FUNCT_4:def 1
.= (dom (EL | (G .edgesOutOf {sink}))) \/ {(P . (lenP2g + 1))} by FUNCOP_1:19
.= (G .edgesOutOf {sink}) \/ {(P . (lenP2g + 1))} by PARTFUN1:def 4
.= G .edgesOutOf {sink} by A46, ZFMISC_1:46 ;
then reconsider EO2 = (EL | (G .edgesOutOf {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL))) as Rbag of G .edgesOutOf {sink} by PARTFUN1:def 4, RELAT_1:def 18;
A49: (FF:PushFlow EL,P) . (P . (lenP2g + 1)) = (EL . (P . (lenP2g + 1))) - (P .tolerance EL) by A3, A6, A44, Def17;

now

let e be set ; :: thesis:
assume A50: e in dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) ; :: thesis:
then A51: e in G .edgesOutOf {sink} by PARTFUN1:def 4;
A52: ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = (FF:PushFlow EL,P) . e by A47, A50, FUNCT_1:72;
(the_Source_of G) . e in {sink} by A51, GLIB_000:def 29;
then A53: (the_Source_of G) . e = sink by TARSKI:def 1;

now

per cases ;

suppose A54: e = P . (lenP2g + 1) ; :: thesis:

then e in {(P . (lenP2g + 1))} by TARSKI:def 1;
then e in dom ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL))) by FUNCOP_1:19;
then EO2 . e = ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL))) . (P . (lenP2g + 1)) by A54, FUNCT_4:14
.= ((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL) by FUNCOP_1:87
.= (FF:PushFlow EL,P) . e by A49, A51, A54, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = EO2 . e by A47, A50, FUNCT_1:72; :: thesis:

end;

suppose A55: e <> P . (lenP2g + 1) ; :: thesis:

A56: now

assume e in P .edges() ; :: thesis:
then consider v1, v2 being Vertex of G, m being odd Element of NAT such that
A57: m + 2 <= len P and
A58: v1 = P . m and
A59: e = P . (m + 1) and
A60: v2 = P . (m + 2) and
A61: e Joins v1,v2,G by GLIB_001:104;

now

per cases by A53, A61, GLIB_000:def 15;

suppose A62: v1 = sink ; :: thesis:

A63: (m + 2) - 2 < (len P) - 0 by A57, XREAL_1:17;
P . m = P . (len P) by A2, A58, A62, GLIB_001:18;
then m = 1 by A63, GLIB_001:def 28;
hence contradiction by A1, A2, A58, A62, GLIB_001:18; :: thesis:

end;

suppose v2 = sink ; :: thesis:

then A64: P . (m + 2) = P . (len P) by A2, A60, GLIB_001:18;

now

assume m + 2 < len P ; :: thesis:
then m + 2 = 1 by A64, GLIB_001:def 28;
then 1 <= 1 - 2 by ABIAN:12;
hence contradiction ; :: thesis:

end;

then m + 2 = len P by A57, XXREAL_0:1;
hence contradiction by A55, A59; :: thesis:

end;

hence contradiction ; :: thesis:

end;

not e in {(P . (lenP2g + 1))} by A55, TARSKI:def 1;
then not e in dom ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL))) by FUNCOP_1:19;
then EO2 . e = (EL | (G .edgesOutOf {sink})) . e by FUNCT_4:12
.= EL . e by A51, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = EO2 . e by A3, A51, A52, A56, Def17; :: thesis:

end;

hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = EO2 . e ; :: thesis:

end;

then A65: Sum ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) = ((Sum (EL | (G .edgesOutOf {sink}))) + (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL))) - ((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) by A48, A47, FUNCT_1:9, GLIB_004:9
.= (Sum (EL | (G .edgesOutOf {sink}))) - (P .tolerance EL) ;
A66: dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) = G .edgesInto {sink} by PARTFUN1:def 4;

A67: now

let e be set ; :: thesis:
assume A68: e in dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) ; :: thesis:
then A69: e in G .edgesInto {sink} by PARTFUN1:def 4;
then (the_Target_of G) . e in {sink} by GLIB_000:def 28;
then A70: (the_Target_of G) . e = sink by TARSKI:def 1;

now

assume e in P .edges() ; :: thesis:
then consider v1, v2 being Vertex of G, m being odd Element of NAT such that
A71: m + 2 <= len P and
A72: v1 = P . m and
A73: e = P . (m + 1) and
A74: v2 = P . (m + 2) and
A75: e Joins v1,v2,G by GLIB_001:104;

now

per cases by A70, A75, GLIB_000:def 15;

suppose A76: v1 = sink ; :: thesis:

A77: (m + 2) - 2 < (len P) - 0 by A71, XREAL_1:17;
P . m = P . (len P) by A2, A72, A76, GLIB_001:18;
then m = 1 by A77, GLIB_001:def 28;
hence contradiction by A1, A2, A72, A76, GLIB_001:18; :: thesis:

end;

suppose v2 = sink ; :: thesis:

then A78: P . (m + 2) = P . (len P) by A2, A74, GLIB_001:18;

now

assume m + 2 < len P ; :: thesis:
then m + 2 = 1 by A78, GLIB_001:def 28;
then 1 <= 1 - 2 by ABIAN:12;
hence contradiction ; :: thesis:

end;

then m + 2 = len P by A71, XXREAL_0:1;
then A79: P . lenP2g = sink by A45, A70, A73, GLIB_000:def 16;
then lenP2g = 1 by A6, A5, GLIB_001:def 28;
hence contradiction by A1, A2, A79, GLIB_001:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then (FF:PushFlow EL,P) . e = EL . e by A3, A69, Def17
.= (EL | (G .edgesInto {sink})) . e by A69, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = (EL | (G .edgesInto {sink})) . e by A66, A68, FUNCT_1:72; :: thesis:

end;

dom (EL | (G .edgesInto {sink})) = G .edgesInto {sink} by PARTFUN1:def 4;
hence (FF:PushFlow EL,P) .flow source,sink = (Sum (EL | (G .edgesInto {sink}))) - ((Sum (EL | (G .edgesOutOf {sink}))) - (P .tolerance EL)) by A65, A66, A67, FUNCT_1:9
.= ((Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})))) + (P .tolerance EL)
.= (EL .flow source,sink) + (P .tolerance EL) ;
:: thesis:

end;

hence (EL .flow source,sink) + (P .tolerance EL) = (FF:PushFlow EL,P) .flow source,sink ; :: thesis: