let G be finite natural-weighted WGraph; :: thesis:
let EL be FF:ELabeling of ; :: thesis:
let source, sink be set ; :: thesis:
let P be Path of G; :: thesis:
assume that
A1: source <> sink and
A1a: EL has_valid_flow_from source,sink and
A1b: P is_Walk_from source,sink and
A1c: P is_augmenting_wrt EL ; :: thesis:
set EL2 = FF:PushFlow EL,P;
set T = P .tolerance EL;
set EI1 = EL | (G .edgesInto {sink});
set EO1 = EL | (G .edgesOutOf {sink});
( P .first() = source & P .last() = sink ) by A1b, GLIB_001:def 23;
then not P is trivial by A1, 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);
A3: lenP2g < (len P) - 0 by XREAL_1:17;
then A4: P . (lenP2g + 1) Joins P . lenP2g,P . (lenP2g + 2),G by GLIB_001:def 3;
then A5: P . (lenP2g + 1) in the_Edges_of G by GLIB_000:def 15;
A7: P . (len P) = sink by A1b, GLIB_001:18;

now

per cases ;

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

then A9: (FF:PushFlow EL,P) . (P . (lenP2g + 1)) = (EL . (P . (lenP2g + 1))) + (P .tolerance EL) by A1c, A3, Def20;
(the_Target_of G) . (P . (lenP2g + 1)) = P . (lenP2g + 2) by A8, GLIB_000:def 16
.= sink by A1b, 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 A5, 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 ((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 by PARTFUN1:def 4, RELAT_1:def 18;
A12: dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) = G .edgesInto {sink} by PARTFUN1:def 4;

now

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

now

per cases ;

suppose A17: 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 A17, 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 A9, A14, A17, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = EI2 . e by A12, A13, A17, FUNCT_1:72; :: thesis:

end;

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

then not e in {(P . (lenP2g + 1))} by 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 A19: EI2 . e = (EL | (G .edgesInto {sink})) . e by FUNCT_4:12
.= EL . e by A14, FUNCT_1:72 ;

now

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

now

per cases by A16, A20, GLIB_000:def 15;

suppose A21: v1 = sink ; :: thesis:

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

end;

suppose v2 = sink ; :: thesis:

then A23: P . (m + 2) = P . (len P) by A1b, A20, GLIB_001:18;

now

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

end;

then m + 2 = len P by A20, XXREAL_0:1;
hence contradiction by A18, A20; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = EI2 . e by A1c, A14, A15, A19, Def20; :: thesis:

end;

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

end;

then A24: 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 A11, A12, FUNCT_1:9, GLIB_004:9
.= (Sum (EL | (G .edgesInto {sink}))) + (P .tolerance EL) ;
A25: ( dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} & dom (EL | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} ) by PARTFUN1:def 4;

now

let e be set ; :: thesis:
assume A26: e in dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) ; :: thesis:
then A27: e in G .edgesOutOf {sink} by PARTFUN1:def 4;
then (the_Source_of G) . e in {sink} by GLIB_000:def 29;
then A28: (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
A29: ( m + 2 <= len P & v1 = P . m & e = P . (m + 1) & v2 = P . (m + 2) & e Joins v1,v2,G ) by GLIB_001:104;

now

per cases by A28, A29, GLIB_000:def 15;

suppose A30: v1 = sink ; :: thesis:

then A31: P . m = P . (len P) by A1b, A29, GLIB_001:18;
(m + 2) - 2 < (len P) - 0 by A29, XREAL_1:17;
then m = 1 by A31, GLIB_001:def 28;
hence contradiction by A1, A1b, A29, A30, GLIB_001:18; :: thesis:

end;

suppose v2 = sink ; :: thesis:

then A32: P . (m + 2) = P . (len P) by A1b, A29, GLIB_001:18;

now

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

end;

then m + 2 = len P by A29, XXREAL_0:1;
then A33: P . lenP2g = sink by A8, A28, A29, GLIB_000:def 16;
then lenP2g = 1 by A3, A7, GLIB_001:def 28;
hence contradiction by A1, A1b, A33, GLIB_001:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then (FF:PushFlow EL,P) . e = EL . e by A1c, A27, Def20
.= (EL | (G .edgesOutOf {sink})) . e by A27, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = (EL | (G .edgesOutOf {sink})) . e by A25, A26, FUNCT_1:72; :: thesis:

end;

then Sum ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) = Sum (EL | (G .edgesOutOf {sink})) by A25, FUNCT_1:9;
hence (FF:PushFlow EL,P) .flow source,sink = ((Sum (EL | (G .edgesInto {sink}))) + (P .tolerance EL)) - (Sum (EL | (G .edgesOutOf {sink}))) by A1, A1a, A1b, A1c, A24, Def8, Th15
.= ((Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})))) + (P .tolerance EL)
.= (EL .flow source,sink) + (P .tolerance EL) by A1a, Def8 ;
:: thesis:

end;

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

then A35: (FF:PushFlow EL,P) . (P . (lenP2g + 1)) = (EL . (P . (lenP2g + 1))) - (P .tolerance EL) by A1c, A3, Def20;
A36: P . (lenP2g + 1) DJoins P . (lenP2g + 2),P . lenP2g,G by A4, A34, GLIB_000:19;
then (the_Source_of G) . (P . (lenP2g + 1)) = P . (lenP2g + 2) by GLIB_000:def 16
.= sink by A1b, GLIB_001:18 ;
then (the_Source_of G) . (P . (lenP2g + 1)) in {sink} by TARSKI:def 1;
then A37: P . (lenP2g + 1) in G .edgesOutOf {sink} by A5, GLIB_000:def 29;
set EO2 = (EL | (G .edgesOutOf {sink})) +* ((P . (lenP2g + 1)) .--> (((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL)));
A38: 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 A37, 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 by PARTFUN1:def 4, RELAT_1:def 18;
A39: dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} by PARTFUN1:def 4;

now

let e be set ; :: thesis:
assume A40: e in dom ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) ; :: thesis:
then A41: e in G .edgesOutOf {sink} by PARTFUN1:def 4;
A42: ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = (FF:PushFlow EL,P) . e by A39, A40, FUNCT_1:72;
(the_Source_of G) . e in {sink} by A41, GLIB_000:def 29;
then A43: (the_Source_of G) . e = sink by TARSKI:def 1;

now

per cases ;

suppose A44: 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 A44, FUNCT_4:14
.= ((EL | (G .edgesOutOf {sink})) . (P . (lenP2g + 1))) - (P .tolerance EL) by FUNCOP_1:87
.= (FF:PushFlow EL,P) . e by A35, A41, A44, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = EO2 . e by A39, A40, FUNCT_1:72; :: thesis:

end;

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

then not e in {(P . (lenP2g + 1))} by 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 A46: EO2 . e = (EL | (G .edgesOutOf {sink})) . e by FUNCT_4:12
.= EL . e by A41, FUNCT_1:72 ;

now

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

now

per cases by A43, A47, GLIB_000:def 15;

suppose A48: v1 = sink ; :: thesis:

then A49: P . m = P . (len P) by A1b, A47, GLIB_001:18;
(m + 2) - 2 < (len P) - 0 by A47, XREAL_1:17;
then m = 1 by A49, GLIB_001:def 28;
hence contradiction by A1, A1b, A47, A48, GLIB_001:18; :: thesis:

end;

suppose v2 = sink ; :: thesis:

then A50: P . (m + 2) = P . (len P) by A1b, A47, GLIB_001:18;

now

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

end;

then m + 2 = len P by A47, XXREAL_0:1;
hence contradiction by A45, A47; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence ((FF:PushFlow EL,P) | (G .edgesOutOf {sink})) . e = EO2 . e by A1c, A41, A42, A46, Def20; :: thesis:

end;

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

end;

then A51: 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 A38, A39, FUNCT_1:9, GLIB_004:9
.= (Sum (EL | (G .edgesOutOf {sink}))) - (P .tolerance EL) ;
A52: ( dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) = G .edgesInto {sink} & dom (EL | (G .edgesInto {sink})) = G .edgesInto {sink} ) by PARTFUN1:def 4;

now

let e be set ; :: thesis:
assume A53: e in dom ((FF:PushFlow EL,P) | (G .edgesInto {sink})) ; :: thesis:
then A54: e in G .edgesInto {sink} by PARTFUN1:def 4;
then (the_Target_of G) . e in {sink} by GLIB_000:def 28;
then A55: (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
A56: ( m + 2 <= len P & v1 = P . m & e = P . (m + 1) & v2 = P . (m + 2) & e Joins v1,v2,G ) by GLIB_001:104;

now

per cases by A55, A56, GLIB_000:def 15;

suppose A57: v1 = sink ; :: thesis:

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

end;

suppose v2 = sink ; :: thesis:

then A59: P . (m + 2) = P . (len P) by A1b, A56, GLIB_001:18;

now

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

end;

then m + 2 = len P by A56, XXREAL_0:1;
then A60: P . lenP2g = sink by A36, A55, A56, GLIB_000:def 16;
then lenP2g = 1 by A3, A7, GLIB_001:def 28;
hence contradiction by A1, A1b, A60, GLIB_001:18; :: thesis:

end;

hence contradiction ; :: thesis:

end;

then (FF:PushFlow EL,P) . e = EL . e by A1c, A54, Def20
.= (EL | (G .edgesInto {sink})) . e by A54, FUNCT_1:72 ;
hence ((FF:PushFlow EL,P) | (G .edgesInto {sink})) . e = (EL | (G .edgesInto {sink})) . e by A52, A53, FUNCT_1:72; :: thesis:

end;

then Sum ((FF:PushFlow EL,P) | (G .edgesInto {sink})) = Sum (EL | (G .edgesInto {sink})) by A52, FUNCT_1:9;
hence (FF:PushFlow EL,P) .flow source,sink = (Sum (EL | (G .edgesInto {sink}))) - ((Sum (EL | (G .edgesOutOf {sink}))) - (P .tolerance EL)) by A1, A1a, A1b, A1c, A51, Def8, Th15
.= ((Sum (EL | (G .edgesInto {sink}))) - (Sum (EL | (G .edgesOutOf {sink})))) + (P .tolerance EL)
.= (EL .flow source,sink) + (P .tolerance EL) by A1a, Def8 ;
:: thesis:

end;

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