let G be finite natural-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for source, sink being set
for P being Path of G st source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
FF:PushFlow EL,P has_valid_flow_from source,sink
let EL be FF:ELabeling of ; :: thesis: for source, sink being set
for P being Path of G st source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
FF:PushFlow EL,P has_valid_flow_from source,sink
let source, sink be set ; :: thesis: for P being Path of G st source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL holds
FF:PushFlow EL,P has_valid_flow_from source,sink
let P be Path of G; :: thesis: ( source <> sink & EL has_valid_flow_from source,sink & P is_Walk_from source,sink & P is_augmenting_wrt EL implies FF:PushFlow EL,P has_valid_flow_from source,sink )
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: FF:PushFlow EL,P has_valid_flow_from source,sink
set EL2 = FF:PushFlow EL,P;

now

thus ( source is Vertex of G & sink is Vertex of G ) by A1a, Def7; :: thesis: ( ( for e being set st e in the_Edges_of G holds
( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds
Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) ) )

now

let e be set ; :: thesis: ( e in the_Edges_of G implies ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ) )
assume A4: e in the_Edges_of G ; :: thesis: ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e )
then A5: ( 0 <= EL . e & EL . e <= (the_Weight_of G) . e ) by A1a, Def7;

now

per cases ( not e in P .edges() or e in P .edges() ) ;

suppose not e in P .edges() ; :: thesis: ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e )

hence ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ) by A1c, A4, A5, Def20; :: thesis: verum

end;

suppose e in P .edges() ; :: thesis: ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e )

then consider n being odd Element of NAT such that
A6: ( n < len P & P . (n + 1) = e ) by GLIB_001:101;
A7: e Joins P . n,P . (n + 2),G by A6, GLIB_001:def 3;
( P .first() = source & P .last() = sink ) by A1b, GLIB_001:def 23;
then A8: not P is trivial by A1, GLIB_001:128;

A10: now

assume ( e DJoins P . n,P . (n + 2),G & e DJoins P . (n + 2),P . n,G ) ; :: thesis: contradiction
then A11: ( (the_Source_of G) . e = P . n & (the_Source_of G) . e = P . (n + 2) ) by GLIB_000:def 16;
A12: n + 0 < n + 2 by XREAL_1:10;
n + 2 <= len P by A6, GLIB_001:1;
then ( n = 1 & n + 2 = len P ) by A11, A12, GLIB_001:def 28;
then ( P . n = source & P . (n + 2) = sink ) by A1b, GLIB_001:18;
hence contradiction by A1, A11; :: thesis: verum

end;

set PFS = P .flowSeq EL;
set n1div2 = (n + 1) div 2;
( 1 <= n + 1 & n + 1 <= len P ) by A6, NAT_1:11, NAT_1:13;
then ( (n + 1) div 2 in dom (P .edgeSeq() ) & P . (n + 1) = (P .edgeSeq() ) . ((n + 1) div 2) ) by GLIB_001:78;
then A13: (n + 1) div 2 in dom (P .flowSeq EL) by A1c, Def18;
2 divides n + 1 by PEPIN:22;
then A14: 2 * ((n + 1) div 2) = n + 1 by NAT_D:3;
then A15: (2 * ((n + 1) div 2)) - 1 = n ;
A16: (2 * ((n + 1) div 2)) + 1 = n + 2 by A14;

now

per cases ( e DJoins P . n,P . (n + 2),G or e DJoins P . (n + 2),P . n,G ) by A7, GLIB_000:19;

suppose A17: e DJoins P . n,P . (n + 2),G ; :: thesis: ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e )

then A18: (EL . e) + (P .tolerance EL) = (FF:PushFlow EL,P) . e by A1c, A6, Def20;
thus 0 <= (FF:PushFlow EL,P) . e ; :: thesis: (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e
(P .flowSeq EL) . ((n + 1) div 2) = ((the_Weight_of G) . e) - (EL . e) by A1c, A6, A13, A15, A16, A17, Def18;
then ((the_Weight_of G) . e) - (EL . e) in rng (P .flowSeq EL) by A13, FUNCT_1:def 5;
then P .tolerance EL <= ((the_Weight_of G) . e) - (EL . e) by A1c, A8, Def19;
then (FF:PushFlow EL,P) . e <= (((the_Weight_of G) . e) - (EL . e)) + (EL . e) by A18, XREAL_1:9;
hence (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ; :: thesis: verum

end;

suppose e DJoins P . (n + 2),P . n,G ; :: thesis: ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e )

then A20: (FF:PushFlow EL,P) . e = (EL . e) - (P .tolerance EL) by A1c, A6, A10, Def20;
thus 0 <= (FF:PushFlow EL,P) . e ; :: thesis: (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e
(FF:PushFlow EL,P) . e <= (EL . e) - 0 by A20, XREAL_1:15;
hence (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ) ; :: thesis: verum

end;

end;

end;

hence ( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ) ; :: thesis: verum

end;

hence for e being set st e in the_Edges_of G holds
( 0 <= (FF:PushFlow EL,P) . e & (FF:PushFlow EL,P) . e <= (the_Weight_of G) . e ) ; :: thesis: for v being Vertex of G st v <> source & v <> sink holds
Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))
let v be Vertex of G; :: thesis: ( v <> source & v <> sink implies Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) )
assume A21: ( v <> source & v <> sink ) ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))
A23: Sum (EL | (v .edgesIn() )) = Sum (EL | (v .edgesOut() )) by A1a, A21, Def7;

now

per cases ( v in P .vertices() or not v in P .vertices() ) ;

suppose v in P .vertices() ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))

then consider n being odd Element of NAT such that
A24: ( n <= len P & P . n = v ) by GLIB_001:88;

A25: now

assume n = len P ; :: thesis: contradiction
then v = P .last() by A24, GLIB_001:def 7
.= sink by A1b, GLIB_001:def 23 ;
hence contradiction by A21; :: thesis: verum

end;

then A26: n < len P by A24, XXREAL_0:1;
A27: 1 <= n by HEYTING3:1;

A28: now

assume n = 1 ; :: thesis: contradiction
then v = P .first() by A24, GLIB_001:def 6
.= source by A1b, GLIB_001:def 23 ;
hence contradiction by A21; :: thesis: verum

end;

then 1 < n by A27, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then reconsider n2 = n - (2 * 1) as odd Element of NAT by INT_1:18;
set e1 = P . (n2 + 1);
set e2 = P . (n + 1);
set T = P .tolerance EL;
A29: n2 < (len P) - 0 by A24, XREAL_1:17;
then A30: P . (n2 + 1) Joins P . n2,P . (n2 + 2),G by GLIB_001:def 3;
A31: P . (n + 1) Joins v,P . (n + 2),G by A24, A26, GLIB_001:def 3;
A32: P . (n2 + 2) = v by A24;

A33: now

assume A34: P . n2 = v ; :: thesis: contradiction
n2 < n - 0 by XREAL_1:17;
hence contradiction by A24, A25, A34, GLIB_001:def 28; :: thesis: verum

end;

A35: now

assume A36: v = P . (n + 2) ; :: thesis: contradiction
A37: n + 0 < n + 2 by XREAL_1:10;
n + 2 <= len P by A26, GLIB_001:1;
hence contradiction by A24, A28, A36, A37, GLIB_001:def 28; :: thesis: verum

end;

A38: now

assume A39: ( P . (n2 + 1) DJoins P . n2,v,G & P . (n2 + 1) DJoins v,P . n2,G ) ; :: thesis: contradiction
then P . n2 = (the_Source_of G) . (P . (n2 + 1)) by GLIB_000:def 16
.= v by A39, GLIB_000:def 16 ;
hence contradiction by A33; :: thesis: verum

end;

A40: now

assume A41: ( P . (n + 1) DJoins v,P . (n + 2),G & P . (n + 1) DJoins P . (n + 2),v,G ) ; :: thesis: contradiction
then A42: P . n = (the_Source_of G) . (P . (n + 1)) by A24, GLIB_000:def 16
.= P . (n + 2) by A41, GLIB_000:def 16 ;
A43: n + 0 < n + 2 by XREAL_1:10;
n + 2 <= len P by A26, GLIB_001:1;
hence contradiction by A28, A42, A43, GLIB_001:def 28; :: thesis: verum

end;

n2 < n - 0 by XREAL_1:17;
then ( 1 <= n2 + 1 & n2 + 1 < n + 1 & n + 1 <= len P ) by A26, NAT_1:11, NAT_1:13, XREAL_1:10;
then A44: P . (n2 + 1) <> P . (n + 1) by GLIB_001:139;

A45: now

let e be set ; :: thesis: ( ( e in v .edgesIn() or e in v .edgesOut() ) & e <> P . (n2 + 1) & e <> P . (n + 1) implies not e in P .edges() )
assume A46: ( ( e in v .edgesIn() or e in v .edgesOut() ) & e <> P . (n2 + 1) & e <> P . (n + 1) ) ; :: thesis: not e in P .edges()

now

assume e in P .edges() ; :: thesis: contradiction
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;
A48: (m + 2) - 2 < (len P) - 0 by A47, XREAL_1:17;

A49: now

per cases ( e in v .edgesIn() or e in v .edgesOut() ) by A46;

suppose e in v .edgesIn() ; :: thesis: ( v1 = v or v2 = v )

then (the_Target_of G) . e = v by GLIB_000:59;
hence ( v1 = v or v2 = v ) by A47, GLIB_000:def 15; :: thesis: verum

end;

suppose e in v .edgesOut() ; :: thesis: ( v1 = v or v2 = v )

then (the_Source_of G) . e = v by GLIB_000:61;
hence ( v1 = v or v2 = v ) by A47, GLIB_000:def 15; :: thesis: verum

end;

end;

end;

now

per cases ( v1 = v or v2 = v ) by A49;

suppose A50: v1 = v ; :: thesis: contradiction

now

per cases ( m < n or m = n or n < m ) by XXREAL_0:1;

suppose m < n ; :: thesis: contradiction

hence contradiction by A24, A25, A47, A50, GLIB_001:def 28; :: thesis: verum

end;

suppose m = n ; :: thesis: contradiction

hence contradiction by A46, A47; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A24, A47, A48, A50, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A51: v2 = v ; :: thesis: contradiction

now

per cases ( m + 2 < n or m + 2 = n or n < m + 2 ) by XXREAL_0:1;

suppose m + 2 < n ; :: thesis: contradiction

hence contradiction by A24, A25, A47, A51, GLIB_001:def 28; :: thesis: verum

end;

suppose m + 2 = n ; :: thesis: contradiction

hence contradiction by A46, A47; :: thesis: verum

end;

suppose n < m + 2 ; :: thesis: contradiction

hence contradiction by A24, A28, A47, A51, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence not e in P .edges() ; :: thesis: verum

end;

now

per cases ( ( P . (n2 + 1) DJoins P . n2,v,G & P . (n + 1) DJoins v,P . (n + 2),G ) or ( P . (n2 + 1) DJoins P . n2,v,G & P . (n + 1) DJoins P . (n + 2),v,G ) or ( P . (n2 + 1) DJoins v,P . n2,G & P . (n + 1) DJoins v,P . (n + 2),G ) or ( P . (n2 + 1) DJoins v,P . n2,G & P . (n + 1) DJoins P . (n + 2),v,G ) ) by A24, A30, A31, GLIB_000:19;

suppose A52: ( P . (n2 + 1) DJoins P . n2,v,G & P . (n + 1) DJoins v,P . (n + 2),G ) ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))

set XIN = (EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)));
set XOUT = (EL | (v .edgesOut() )) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL)));
A53: ( P . (n2 + 1) in v .edgesIn() & P . (n + 1) in v .edgesOut() ) by A52, GLIB_000:60, GLIB_000:62;
A54: dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) = {(P . (n2 + 1))} by FUNCOP_1:19;
then A55: dom ((EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)))) = (dom (EL | (v .edgesIn() ))) \/ {(P . (n2 + 1))} by FUNCT_4:def 1
.= (v .edgesIn() ) \/ {(P . (n2 + 1))} by PARTFUN1:def 4
.= v .edgesIn() by A53, ZFMISC_1:46 ;
then reconsider XIN = (EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A56: dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) = {(P . (n + 1))} by FUNCOP_1:19;
then A57: dom ((EL | (v .edgesOut() )) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL)))) = (dom (EL | (v .edgesOut() ))) \/ {(P . (n + 1))} by FUNCT_4:def 1
.= (v .edgesOut() ) \/ {(P . (n + 1))} by PARTFUN1:def 4
.= v .edgesOut() by A53, ZFMISC_1:46 ;
then reconsider XOUT = (EL | (v .edgesOut() )) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A58: dom ((FF:PushFlow EL,P) | (v .edgesIn() )) = v .edgesIn() by PARTFUN1:def 4;

now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) implies ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN . e )
assume e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN . e
then A59: e in v .edgesIn() by PARTFUN1:def 4;
then A60: (the_Target_of G) . e = v by GLIB_000:59;

now

per cases ( e = P . (n2 + 1) or e <> P . (n2 + 1) ) ;

suppose A61: e = P . (n2 + 1) ; :: thesis: XIN . e = (FF:PushFlow EL,P) . e

then e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by A54, TARSKI:def 1;
hence XIN . e = ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) . (P . (n2 + 1)) by A61, FUNCT_4:14
.= (EL . (P . (n2 + 1))) + (P .tolerance EL) by FUNCOP_1:87
.= (FF:PushFlow EL,P) . e by A1c, A29, A32, A52, A61, Def20 ;
:: thesis: verum

end;

suppose A62: e <> P . (n2 + 1) ; :: thesis: (FF:PushFlow EL,P) . e = XIN . e

then not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by A54, TARSKI:def 1;
then A63: XIN . e = (EL | (v .edgesIn() )) . e by FUNCT_4:12
.= EL . e by A59, FUNCT_1:72 ;

now

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

now

per cases ( v = v1 or v = v2 ) by A60, A64, GLIB_000:def 15;

suppose A66: v = v1 ; :: thesis: contradiction

now

per cases ( m < n or m = n or n < m ) by XXREAL_0:1;

suppose m < n ; :: thesis: contradiction

hence contradiction by A24, A25, A64, A66, GLIB_001:def 28; :: thesis: verum

end;

suppose m = n ; :: thesis: contradiction

then A67: P . (n + 2) = P . n by A24, A52, A60, A64, GLIB_000:def 16;
A68: (n + 2) - 2 < (n + 2) - 0 by XREAL_1:17;
n + 2 <= len P by A26, GLIB_001:1;
hence contradiction by A28, A67, A68, GLIB_001:def 28; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A24, A64, A65, A66, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A69: v = v2 ; :: thesis: contradiction

now

per cases ( m + 2 < n or m + 2 = n or n < m + 2 ) by XXREAL_0:1;

suppose m + 2 < n ; :: thesis: contradiction

hence contradiction by A24, A25, A64, A69, GLIB_001:def 28; :: thesis: verum

end;

suppose m + 2 = n ; :: thesis: contradiction

hence contradiction by A62, A64; :: thesis: verum

end;

suppose n < m + 2 ; :: thesis: contradiction

hence contradiction by A24, A28, A64, A69, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence (FF:PushFlow EL,P) . e = XIN . e by A1c, A59, A63, Def20; :: thesis: verum

end;

end;

end;

hence ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN . e by A59, FUNCT_1:72; :: thesis: verum

end;

then A70: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum XIN by A55, A58, FUNCT_1:9;
A71: dom ((FF:PushFlow EL,P) | (v .edgesOut() )) = v .edgesOut() by PARTFUN1:def 4;

A72: now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) implies ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT . e )
assume e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT . e
then A73: e in v .edgesOut() by PARTFUN1:def 4;
then A74: (the_Source_of G) . e = v by GLIB_000:61;

now

per cases ( e = P . (n + 1) or e <> P . (n + 1) ) ;

suppose A75: e = P . (n + 1) ; :: thesis: XOUT . e = (FF:PushFlow EL,P) . e

then e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A56, TARSKI:def 1;
hence XOUT . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) . (P . (n + 1)) by A75, FUNCT_4:14
.= (EL . (P . (n + 1))) + (P .tolerance EL) by FUNCOP_1:87
.= (FF:PushFlow EL,P) . e by A1c, A24, A26, A52, A75, Def20 ;
:: thesis: verum

end;

suppose A76: e <> P . (n + 1) ; :: thesis: (FF:PushFlow EL,P) . e = XOUT . e

then not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A56, TARSKI:def 1;
then A77: XOUT . e = (EL | (v .edgesOut() )) . e by FUNCT_4:12
.= EL . e by A73, FUNCT_1:72 ;

now

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

now

per cases ( v = v1 or v = v2 ) by A74, A78, GLIB_000:def 15;

suppose A80: v = v1 ; :: thesis: contradiction

now

per cases ( m < n or m = n or n < m ) by XXREAL_0:1;

suppose m < n ; :: thesis: contradiction

hence contradiction by A24, A25, A78, A80, GLIB_001:def 28; :: thesis: verum

end;

suppose m = n ; :: thesis: contradiction

hence contradiction by A76, A78; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A24, A78, A79, A80, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A81: v = v2 ; :: thesis: contradiction

now

per cases ( m + 2 < n or m + 2 = n or n < m + 2 ) by XXREAL_0:1;

suppose m + 2 < n ; :: thesis: contradiction

hence contradiction by A24, A25, A78, A81, GLIB_001:def 28; :: thesis: verum

end;

suppose m + 2 = n ; :: thesis: contradiction

then A82: P . n2 = P . n by A24, A52, A74, A78, GLIB_000:def 16;
n2 < n - 0 by XREAL_1:17;
hence contradiction by A24, A25, A82, GLIB_001:def 28; :: thesis: verum

end;

suppose n < m + 2 ; :: thesis: contradiction

hence contradiction by A24, A28, A78, A81, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence (FF:PushFlow EL,P) . e = XOUT . e by A1c, A73, A77, Def20; :: thesis: verum

end;

end;

end;

hence ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT . e by A73, FUNCT_1:72; :: thesis: verum

end;

Sum XIN = ((Sum (EL | (v .edgesIn() ))) + ((P .tolerance EL) + (EL . (P . (n2 + 1))))) - ((EL | (v .edgesIn() )) . (P . (n2 + 1))) by GLIB_004:9
.= (((Sum (EL | (v .edgesOut() ))) + (P .tolerance EL)) + (EL . (P . (n2 + 1)))) - (EL . (P . (n2 + 1))) by A23, A53, FUNCT_1:72
.= (((Sum (EL | (v .edgesOut() ))) + (P .tolerance EL)) + (EL . (P . (n + 1)))) - (EL . (P . (n + 1)))
.= ((Sum (EL | (v .edgesOut() ))) + ((P .tolerance EL) + (EL . (P . (n + 1))))) - ((EL | (v .edgesOut() )) . (P . (n + 1))) by A53, FUNCT_1:72
.= Sum XOUT by GLIB_004:9 ;
hence Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) by A57, A70, A71, A72, FUNCT_1:9; :: thesis: verum

end;

suppose A83: ( P . (n2 + 1) DJoins P . n2,v,G & P . (n + 1) DJoins P . (n + 2),v,G ) ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))

then A84: ( (FF:PushFlow EL,P) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) + (P .tolerance EL) & (FF:PushFlow EL,P) . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) by A1c, A26, A29, A32, A40, Def20;
A85: ( P . (n2 + 1) in v .edgesIn() & P . (n + 1) in v .edgesIn() ) by A83, GLIB_000:60;
set XIN1 = (EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)));
set XIN2 = ((EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)))) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL)));
A86: dom ((EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)))) = (dom (EL | (v .edgesIn() ))) \/ (dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)))) by FUNCT_4:def 1
.= (dom (EL | (v .edgesIn() ))) \/ {(P . (n2 + 1))} by FUNCOP_1:19
.= (v .edgesIn() ) \/ {(P . (n2 + 1))} by PARTFUN1:def 4
.= v .edgesIn() by A85, ZFMISC_1:46 ;
then reconsider XIN1 = (EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A87: dom (((EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)))) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL)))) = (dom XIN1) \/ (dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL)))) by FUNCT_4:def 1
.= (v .edgesIn() ) \/ {(P . (n + 1))} by A86, FUNCOP_1:19
.= v .edgesIn() by A85, ZFMISC_1:46 ;
then reconsider XIN2 = ((EL | (v .edgesIn() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL)))) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A88: dom ((FF:PushFlow EL,P) | (v .edgesIn() )) = v .edgesIn() by PARTFUN1:def 4;
A89: ( dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) = {(P . (n2 + 1))} & dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) = {(P . (n + 1))} ) by FUNCOP_1:19;

A90: now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) implies ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e )
assume A91: e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e
then A92: e in v .edgesIn() by PARTFUN1:def 4;
A93: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = (FF:PushFlow EL,P) . e by A88, A91, FUNCT_1:72;

now

per cases ( e = P . (n2 + 1) or e = P . (n + 1) or ( e <> P . (n2 + 1) & e <> P . (n + 1) ) ) ;

suppose A94: e = P . (n2 + 1) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e

then A95: ( not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) & e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) ) by A44, A89, TARSKI:def 1;
then XIN2 . e = XIN1 . e by FUNCT_4:12
.= ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) . e by A95, FUNCT_4:14
.= (FF:PushFlow EL,P) . e by A84, A94, FUNCOP_1:87 ;
hence ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e by A88, A91, FUNCT_1:72; :: thesis: verum

end;

suppose A96: e = P . (n + 1) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e

then e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) by A89, TARSKI:def 1;
then XIN2 . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) . (P . (n + 1)) by A96, FUNCT_4:14
.= (FF:PushFlow EL,P) . e by A84, A96, FUNCOP_1:87 ;
hence ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e by A88, A91, FUNCT_1:72; :: thesis: verum

end;

suppose A97: ( e <> P . (n2 + 1) & e <> P . (n + 1) ) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e

then A98: ( not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) & not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) ) by A89, TARSKI:def 1;
then A99: XIN2 . e = XIN1 . e by FUNCT_4:12
.= (EL | (v .edgesIn() )) . e by A98, FUNCT_4:12
.= EL . e by A92, FUNCT_1:72 ;
not e in P .edges() by A45, A92, A97;
hence ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e by A1c, A92, A93, A99, Def20; :: thesis: verum

end;

end;

end;

hence ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = XIN2 . e ; :: thesis: verum

end;

not P . (n + 1) in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by A44, A89, TARSKI:def 1;
then A100: XIN1 . (P . (n + 1)) = (EL | (v .edgesIn() )) . (P . (n + 1)) by FUNCT_4:12
.= EL . (P . (n + 1)) by A85, FUNCT_1:72 ;
A101: ( dom ((FF:PushFlow EL,P) | (v .edgesOut() )) = v .edgesOut() & dom (EL | (v .edgesOut() )) = v .edgesOut() ) by PARTFUN1:def 4;

now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) implies ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = (EL | (v .edgesOut() )) . e )
assume A102: e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = (EL | (v .edgesOut() )) . e
then A103: e in v .edgesOut() by PARTFUN1:def 4;
A104: ( ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = (FF:PushFlow EL,P) . e & (EL | (v .edgesOut() )) . e = EL . e ) by A101, A102, FUNCT_1:72;
A105: ( e in the_Edges_of G & (the_Source_of G) . e = v ) by A103, GLIB_000:61;
then A106: e <> P . (n2 + 1) by A33, A83, GLIB_000:def 16;
e <> P . (n + 1) by A35, A83, A105, GLIB_000:def 16;
then not e in P .edges() by A45, A103, A106;
hence ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = (EL | (v .edgesOut() )) . e by A1c, A103, A104, Def20; :: thesis: verum

end;

then A107: (FF:PushFlow EL,P) | (v .edgesOut() ) = EL | (v .edgesOut() ) by A101, FUNCT_1:9;
Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = ((Sum XIN1) + ((EL . (P . (n + 1))) - (P .tolerance EL))) - (EL . (P . (n + 1))) by A100, A87, A88, A90, FUNCT_1:9, GLIB_004:9
.= (Sum XIN1) - ((EL . (P . (n + 1))) - ((EL . (P . (n + 1))) - (P .tolerance EL)))
.= (((Sum (EL | (v .edgesIn() ))) + ((EL . (P . (n2 + 1))) + (P .tolerance EL))) - ((EL | (v .edgesIn() )) . (P . (n2 + 1)))) - (P .tolerance EL) by GLIB_004:9
.= ((((Sum (EL | (v .edgesIn() ))) + (P .tolerance EL)) + (EL . (P . (n2 + 1)))) - (EL . (P . (n2 + 1)))) - (P .tolerance EL) by A85, FUNCT_1:72
.= Sum (EL | (v .edgesIn() )) ;
hence Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) by A1a, A21, A107, Def7; :: thesis: verum

end;

suppose A108: ( P . (n2 + 1) DJoins v,P . n2,G & P . (n + 1) DJoins v,P . (n + 2),G ) ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))

then A109: ( (FF:PushFlow EL,P) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) - (P .tolerance EL) & (FF:PushFlow EL,P) . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) ) by A1c, A26, A29, A32, A38, Def20;
A110: ( P . (n2 + 1) in v .edgesOut() & P . (n + 1) in v .edgesOut() ) by A108, GLIB_000:62;
set XOUT1 = (EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)));
set XOUT2 = ((EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL)));
A111: dom ((EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) = (dom (EL | (v .edgesOut() ))) \/ (dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) by FUNCT_4:def 1
.= (dom (EL | (v .edgesOut() ))) \/ {(P . (n2 + 1))} by FUNCOP_1:19
.= (v .edgesOut() ) \/ {(P . (n2 + 1))} by PARTFUN1:def 4
.= v .edgesOut() by A110, ZFMISC_1:46 ;
then reconsider XOUT1 = (EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A112: dom (((EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL)))) = (dom XOUT1) \/ (dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL)))) by FUNCT_4:def 1
.= (v .edgesOut() ) \/ {(P . (n + 1))} by A111, FUNCOP_1:19
.= v .edgesOut() by A110, ZFMISC_1:46 ;
then reconsider XOUT2 = ((EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A113: dom ((FF:PushFlow EL,P) | (v .edgesOut() )) = v .edgesOut() by PARTFUN1:def 4;
A114: ( dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) = {(P . (n2 + 1))} & dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) = {(P . (n + 1))} ) by FUNCOP_1:19;

A115: now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) implies ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e )
assume A116: e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e
then A117: e in v .edgesOut() by PARTFUN1:def 4;
A118: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = (FF:PushFlow EL,P) . e by A113, A116, FUNCT_1:72;

now

per cases ( e = P . (n2 + 1) or e = P . (n + 1) or ( e <> P . (n2 + 1) & e <> P . (n + 1) ) ) ;

suppose A119: e = P . (n2 + 1) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e

then A120: ( not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) & e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) ) by A44, A114, TARSKI:def 1;
then XOUT2 . e = XOUT1 . e by FUNCT_4:12
.= ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) . e by A120, FUNCT_4:14
.= (FF:PushFlow EL,P) . e by A109, A119, FUNCOP_1:87 ;
hence ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e by A113, A116, FUNCT_1:72; :: thesis: verum

end;

suppose A121: e = P . (n + 1) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e

then e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A114, TARSKI:def 1;
then XOUT2 . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) . e by FUNCT_4:14
.= (FF:PushFlow EL,P) . e by A109, A121, FUNCOP_1:87 ;
hence ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e by A113, A116, FUNCT_1:72; :: thesis: verum

end;

suppose A122: ( e <> P . (n2 + 1) & e <> P . (n + 1) ) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e

then A123: ( not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) & not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) ) by A114, TARSKI:def 1;
then A124: XOUT2 . e = XOUT1 . e by FUNCT_4:12
.= (EL | (v .edgesOut() )) . e by A123, FUNCT_4:12
.= EL . e by A117, FUNCT_1:72 ;
not e in P .edges() by A45, A117, A122;
hence ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e by A1c, A117, A118, A124, Def20; :: thesis: verum

end;

end;

end;

hence ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = XOUT2 . e ; :: thesis: verum

end;

not P . (n + 1) in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) by A44, A114, TARSKI:def 1;
then A125: XOUT1 . (P . (n + 1)) = (EL | (v .edgesOut() )) . (P . (n + 1)) by FUNCT_4:12
.= EL . (P . (n + 1)) by A110, FUNCT_1:72 ;
A126: Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) = ((Sum XOUT1) + ((EL . (P . (n + 1))) + (P .tolerance EL))) - (EL . (P . (n + 1))) by A125, A112, A113, A115, FUNCT_1:9, GLIB_004:9
.= (((Sum XOUT1) - (EL . (P . (n + 1)))) + (EL . (P . (n + 1)))) + (P .tolerance EL)
.= (((Sum (EL | (v .edgesOut() ))) + ((EL . (P . (n2 + 1))) - (P .tolerance EL))) - ((EL | (v .edgesOut() )) . (P . (n2 + 1)))) + (P .tolerance EL) by GLIB_004:9
.= ((((Sum (EL | (v .edgesOut() ))) + (EL . (P . (n2 + 1)))) - (P .tolerance EL)) - (EL . (P . (n2 + 1)))) + (P .tolerance EL) by A110, FUNCT_1:72
.= Sum (EL | (v .edgesOut() )) ;
A127: ( dom ((FF:PushFlow EL,P) | (v .edgesIn() )) = v .edgesIn() & dom (EL | (v .edgesIn() )) = v .edgesIn() ) by PARTFUN1:def 4;

now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) implies ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = (EL | (v .edgesIn() )) . e )
assume A128: e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) ; :: thesis: ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = (EL | (v .edgesIn() )) . e
then A129: e in v .edgesIn() by PARTFUN1:def 4;
A130: ( ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = (FF:PushFlow EL,P) . e & (EL | (v .edgesIn() )) . e = EL . e ) by A127, A128, FUNCT_1:72;
A131: ( e in the_Edges_of G & (the_Target_of G) . e = v ) by A129, GLIB_000:59;
then A132: e <> P . (n2 + 1) by A33, A108, GLIB_000:def 16;
e <> P . (n + 1) by A35, A108, A131, GLIB_000:def 16;
then not e in P .edges() by A45, A129, A132;
hence ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = (EL | (v .edgesIn() )) . e by A1c, A129, A130, Def20; :: thesis: verum

end;

hence Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) by A23, A126, A127, FUNCT_1:9; :: thesis: verum

end;

suppose A133: ( P . (n2 + 1) DJoins v,P . n2,G & P . (n + 1) DJoins P . (n + 2),v,G ) ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))

then A134: ( (FF:PushFlow EL,P) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) - (P .tolerance EL) & (FF:PushFlow EL,P) . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) ) by A1c, A26, A29, A32, A38, A40, Def20;
A135: ( P . (n2 + 1) in v .edgesOut() & P . (n + 1) in v .edgesIn() ) by A133, GLIB_000:60, GLIB_000:62;
set XIN = (EL | (v .edgesIn() )) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL)));
set XOUT = (EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)));
A136: ( dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) = {(P . (n2 + 1))} & dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) = {(P . (n + 1))} ) by FUNCOP_1:19;
then A137: dom ((EL | (v .edgesIn() )) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL)))) = (dom (EL | (v .edgesIn() ))) \/ {(P . (n + 1))} by FUNCT_4:def 1
.= (v .edgesIn() ) \/ {(P . (n + 1))} by PARTFUN1:def 4
.= v .edgesIn() by A135, ZFMISC_1:46 ;
then reconsider XIN = (EL | (v .edgesIn() )) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A138: dom ((EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) = (dom (EL | (v .edgesOut() ))) \/ {(P . (n2 + 1))} by A136, FUNCT_4:def 1
.= (v .edgesOut() ) \/ {(P . (n2 + 1))} by PARTFUN1:def 4
.= v .edgesOut() by A135, ZFMISC_1:46 ;
then reconsider XOUT = (EL | (v .edgesOut() )) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) as Rbag of by PARTFUN1:def 4, RELAT_1:def 18;
A139: ( dom ((FF:PushFlow EL,P) | (v .edgesIn() )) = v .edgesIn() & dom ((FF:PushFlow EL,P) | (v .edgesOut() )) = v .edgesOut() ) by PARTFUN1:def 4;

now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) implies XIN . e = ((FF:PushFlow EL,P) | (v .edgesIn() )) . e )
assume e in dom ((FF:PushFlow EL,P) | (v .edgesIn() )) ; :: thesis: XIN . e = ((FF:PushFlow EL,P) | (v .edgesIn() )) . e
then A140: e in v .edgesIn() by PARTFUN1:def 4;
then A141: (the_Target_of G) . e = v by GLIB_000:59;

now

per cases ( e = P . (n + 1) or e <> P . (n + 1) ) ;

suppose A142: e = P . (n + 1) ; :: thesis: XIN . e = (FF:PushFlow EL,P) . e

then e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) by A136, TARSKI:def 1;
hence XIN . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) . (P . (n + 1)) by A142, FUNCT_4:14
.= (FF:PushFlow EL,P) . e by A134, A142, FUNCOP_1:87 ;
:: thesis: verum

end;

suppose A143: e <> P . (n + 1) ; :: thesis: (FF:PushFlow EL,P) . e = XIN . e

then not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) by A136, TARSKI:def 1;
then A144: XIN . e = (EL | (v .edgesIn() )) . e by FUNCT_4:12
.= EL . e by A140, FUNCT_1:72 ;
e <> P . (n2 + 1) by A33, A133, A141, GLIB_000:def 16;
then not e in P .edges() by A45, A140, A143;
hence (FF:PushFlow EL,P) . e = XIN . e by A1c, A140, A144, Def20; :: thesis: verum

end;

end;

end;

hence XIN . e = ((FF:PushFlow EL,P) | (v .edgesIn() )) . e by A140, FUNCT_1:72; :: thesis: verum

end;

then A145: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = ((Sum (EL | (v .edgesIn() ))) + ((EL . (P . (n + 1))) - (P .tolerance EL))) - ((EL | (v .edgesIn() )) . (P . (n + 1))) by A137, A139, FUNCT_1:9, GLIB_004:9
.= (((Sum (EL | (v .edgesIn() ))) + (EL . (P . (n + 1)))) - (P .tolerance EL)) - (EL . (P . (n + 1))) by A135, FUNCT_1:72
.= (Sum (EL | (v .edgesIn() ))) - (P .tolerance EL) ;

now

let e be set ; :: thesis: ( e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) implies XOUT . e = ((FF:PushFlow EL,P) | (v .edgesOut() )) . e )
assume e in dom ((FF:PushFlow EL,P) | (v .edgesOut() )) ; :: thesis: XOUT . e = ((FF:PushFlow EL,P) | (v .edgesOut() )) . e
then A146: e in v .edgesOut() by PARTFUN1:def 4;
then A147: (the_Source_of G) . e = v by GLIB_000:61;

now

per cases ( e = P . (n2 + 1) or e <> P . (n2 + 1) ) ;

suppose A148: e = P . (n2 + 1) ; :: thesis: XOUT . e = (FF:PushFlow EL,P) . e

then e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) by A136, TARSKI:def 1;
hence XOUT . e = ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) . (P . (n2 + 1)) by A148, FUNCT_4:14
.= (FF:PushFlow EL,P) . e by A134, A148, FUNCOP_1:87 ;
:: thesis: verum

end;

suppose A149: e <> P . (n2 + 1) ; :: thesis: (FF:PushFlow EL,P) . e = XOUT . e

then not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) by A136, TARSKI:def 1;
then A150: XOUT . e = (EL | (v .edgesOut() )) . e by FUNCT_4:12
.= EL . e by A146, FUNCT_1:72 ;
e <> P . (n + 1) by A35, A133, A147, GLIB_000:def 16;
then not e in P .edges() by A45, A146, A149;
hence (FF:PushFlow EL,P) . e = XOUT . e by A1c, A146, A150, Def20; :: thesis: verum

end;

end;

end;

hence XOUT . e = ((FF:PushFlow EL,P) | (v .edgesOut() )) . e by A146, FUNCT_1:72; :: thesis: verum

end;

then Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) = ((Sum (EL | (v .edgesOut() ))) + ((EL . (P . (n2 + 1))) - (P .tolerance EL))) - ((EL | (v .edgesOut() )) . (P . (n2 + 1))) by A138, A139, FUNCT_1:9, GLIB_004:9
.= (((Sum (EL | (v .edgesOut() ))) + (EL . (P . (n2 + 1)))) - (P .tolerance EL)) - (EL . (P . (n2 + 1))) by A135, FUNCT_1:72
.= (Sum (EL | (v .edgesIn() ))) - (P .tolerance EL) by A23 ;
hence Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) by A145; :: thesis: verum

end;

end;

end;

hence Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) ; :: thesis: verum

end;

suppose A151: not v in P .vertices() ; :: thesis: Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() ))

A152: dom (EL | (v .edgesIn() )) = v .edgesIn() by PARTFUN1:def 4;
then A153: dom (EL | (v .edgesIn() )) = dom ((FF:PushFlow EL,P) | (v .edgesIn() )) by PARTFUN1:def 4;

A158a: now

let e be set ; :: thesis: ( e in dom (EL | (v .edgesIn() )) implies (EL | (v .edgesIn() )) . e = ((FF:PushFlow EL,P) | (v .edgesIn() )) . e )
assume A154: e in dom (EL | (v .edgesIn() )) ; :: thesis: (EL | (v .edgesIn() )) . e = ((FF:PushFlow EL,P) | (v .edgesIn() )) . e
then A155: ( (EL | (v .edgesIn() )) . e = EL . e & ((FF:PushFlow EL,P) | (v .edgesIn() )) . e = (FF:PushFlow EL,P) . e ) by A152, FUNCT_1:72;

now

assume A156: e in P .edges() ; :: thesis: contradiction
consider x being set such that
A157: e DJoins x,v,G by A152, A154, GLIB_000:60;
e Joins x,v,G by A157, GLIB_000:19;
hence contradiction by A151, A156, GLIB_001:106; :: thesis: verum

end;

hence (EL | (v .edgesIn() )) . e = ((FF:PushFlow EL,P) | (v .edgesIn() )) . e by A1c, A152, A154, A155, Def20; :: thesis: verum

end;

A159: ( dom (EL | (v .edgesOut() )) = v .edgesOut() & dom ((FF:PushFlow EL,P) | (v .edgesOut() )) = v .edgesOut() ) by PARTFUN1:def 4;

now

let e be set ; :: thesis: ( e in dom (EL | (v .edgesOut() )) implies (EL | (v .edgesOut() )) . e = ((FF:PushFlow EL,P) | (v .edgesOut() )) . e )
assume A160: e in dom (EL | (v .edgesOut() )) ; :: thesis: (EL | (v .edgesOut() )) . e = ((FF:PushFlow EL,P) | (v .edgesOut() )) . e
then A161: e in v .edgesOut() by PARTFUN1:def 4;
A162: ( (EL | (v .edgesOut() )) . e = EL . e & ((FF:PushFlow EL,P) | (v .edgesOut() )) . e = (FF:PushFlow EL,P) . e ) by A159, A160, FUNCT_1:72;

now

assume A163: e in P .edges() ; :: thesis: contradiction
consider x being set such that
A164: e DJoins v,x,G by A161, GLIB_000:62;
e Joins v,x,G by A164, GLIB_000:19;
hence contradiction by A151, A163, GLIB_001:106; :: thesis: verum

end;

hence (EL | (v .edgesOut() )) . e = ((FF:PushFlow EL,P) | (v .edgesOut() )) . e by A1c, A161, A162, Def20; :: thesis: verum

end;

then A165: EL | (v .edgesOut() ) = (FF:PushFlow EL,P) | (v .edgesOut() ) by A159, FUNCT_1:9;
thus Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum (EL | (v .edgesIn() )) by A158a, A153, FUNCT_1:9
.= Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) by A165, A1a, A21, Def7 ; :: thesis: verum

end;

end;

end;

hence Sum ((FF:PushFlow EL,P) | (v .edgesIn() )) = Sum ((FF:PushFlow EL,P) | (v .edgesOut() )) ; :: thesis: verum

end;

hence FF:PushFlow EL,P has_valid_flow_from source,sink by Def7; :: thesis: verum