let G be _finite natural-weighted WGraph; :: thesis: for EL being FF:ELabeling of G
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 G; :: 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
A2: EL has_valid_flow_from source,sink and
A3: P is_Walk_from source,sink and
A4: P is_augmenting_wrt EL ; :: thesis: FF:PushFlow (EL,P) has_valid_flow_from source,sink
set EL2 = FF:PushFlow (EL,P);

now :: thesis: ( source is Vertex of G & sink is Vertex of G & ( 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())) ) )

thus ( source is Vertex of G & sink is Vertex of G ) by A2; :: 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 :: 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 )

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 A5: e in the_Edges_of G ; :: thesis: ( 0 <= (FF:PushFlow (EL,P)) . e & (FF:PushFlow (EL,P)) . e <= (the_Weight_of G) . e )
then A6: EL . e <= (the_Weight_of G) . e by A2;

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

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 A4, A5, A6, Def17; :: 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
A7: n < len P and
A8: P . (n + 1) = e by GLIB_001:100;
set PFS = P .flowSeq EL;
set n1div2 = (n + 1) div 2;
A9: 1 <= n + 1 by NAT_1:11;
n + 1 <= len P by A7, NAT_1:13;
then (n + 1) div 2 in dom (P .edgeSeq()) by A9, GLIB_001:77;
then A10: (n + 1) div 2 in dom (P .flowSeq EL) by A4, Def15;

A11: now :: thesis: ( e DJoins P . n,P . (n + 2),G implies not e DJoins P . (n + 2),P . n,G )

A12: n + 0 < n + 2 by XREAL_1:8;
assume that
A13: e DJoins P . n,P . (n + 2),G and
A14: e DJoins P . (n + 2),P . n,G ; :: thesis: contradiction
A15: (the_Source_of G) . e = P . n by A13;
A16: (the_Source_of G) . e = P . (n + 2) by A14;
A17: n + 2 <= len P by A7, GLIB_001:1;
then n = 1 by A15, A16, A12, GLIB_001:def 28;
then A18: P . n = source by A3, GLIB_001:17;
n + 2 = len P by A15, A16, A12, A17, GLIB_001:def 28;
hence contradiction by A1, A3, A15, A16, A18, GLIB_001:17; :: thesis: verum

end;

A19: P .last() = sink by A3, GLIB_001:def 23;
P .first() = source by A3, GLIB_001:def 23;
then A20: P is trivial by A1, A19, GLIB_001:127;
2 divides n + 1 by PEPIN:22;
then A21: 2 * ((n + 1) div 2) = n + 1 by NAT_D:3;
then A22: (2 * ((n + 1) div 2)) - 1 = n ;
A23: (2 * ((n + 1) div 2)) + 1 = n + 2 by A21;
A24: e Joins P . n,P . (n + 2),G by A7, A8, GLIB_001:def 3;

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

per cases ( e DJoins P . n,P . (n + 2),G or e DJoins P . (n + 2),P . n,G ) by A24;

suppose A25: 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 (P .flowSeq EL) . ((n + 1) div 2) = ((the_Weight_of G) . e) - (EL . e) by A4, A8, A10, A22, A23, Def15;
then ((the_Weight_of G) . e) - (EL . e) in rng (P .flowSeq EL) by A10, FUNCT_1:def 3;
then A26: P .tolerance EL <= ((the_Weight_of G) . e) - (EL . e) by A4, A20, Def16;
thus 0 <= (FF:PushFlow (EL,P)) . e ; :: thesis: (FF:PushFlow (EL,P)) . e <= (the_Weight_of G) . e
(EL . e) + (P .tolerance EL) = (FF:PushFlow (EL,P)) . e by A4, A7, A8, A25, Def17;
then (FF:PushFlow (EL,P)) . e <= (((the_Weight_of G) . e) - (EL . e)) + (EL . e) by A26, XREAL_1:7;
hence (FF:PushFlow (EL,P)) . e <= (the_Weight_of G) . e ; :: thesis: verum

end;

suppose A27: 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 )

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) - (P .tolerance EL) by A4, A7, A8, A11, A27, Def17;
then (FF:PushFlow (EL,P)) . e <= (EL . e) - 0 by XREAL_1:13;
hence (FF:PushFlow (EL,P)) . e <= (the_Weight_of G) . e by A6, 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 that
A28: v <> source and
A29: v <> sink ; :: thesis: Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum ((FF:PushFlow (EL,P)) | (v .edgesOut()))
A30: Sum (EL | (v .edgesIn())) = Sum (EL | (v .edgesOut())) by A2, A28, A29;

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

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
A31: n <= len P and
A32: P . n = v by GLIB_001:87;

A33: now :: thesis: not n = len P

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

end;

then A34: n < len P by A31, XXREAL_0:1;

A35: now :: thesis: not n = 1

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

end;

A36: now :: thesis: not v = P . (n + 2)

A37: n + 0 < n + 2 by XREAL_1:8;
assume A38: v = P . (n + 2) ; :: thesis: contradiction
n + 2 <= len P by A34, GLIB_001:1;
hence contradiction by A32, A35, A38, A37, GLIB_001:def 28; :: thesis: verum

end;

1 <= n by ABIAN:12;
then 1 < n by A35, 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:5;
set e1 = P . (n2 + 1);
set e2 = P . (n + 1);
set T = P .tolerance EL;
A39: 1 <= n2 + 1 by NAT_1:11;
A40: P . (n2 + 2) = v by A32;

A41: now :: thesis: for e being set st ( e in v .edgesIn() or e in v .edgesOut() ) & e <> P . (n2 + 1) & e <> P . (n + 1) holds
not e in P .edges()

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 that
A42: ( e in v .edgesIn() or e in v .edgesOut() ) and
A43: e <> P . (n2 + 1) and
A44: e <> P . (n + 1) ; :: thesis: not e in P .edges()

now :: thesis: not e in P .edges()

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

A50: now :: thesis: ( v1 = v or v2 = v )

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

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

then (the_Target_of G) . e = v by GLIB_000:56;
hence ( v1 = v or v2 = v ) by A49; :: thesis: verum

end;

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

then (the_Source_of G) . e = v by GLIB_000:58;
hence ( v1 = v or v2 = v ) by A49; :: thesis: verum

end;

end;

end;

A51: (m + 2) - 2 < (len P) - 0 by A45, XREAL_1:15;

now :: thesis: contradiction

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

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

now :: thesis: contradiction

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

suppose m < n ; :: thesis: contradiction

hence contradiction by A31, A32, A33, A46, A52, GLIB_001:def 28; :: thesis: verum

end;

suppose m = n ; :: thesis: contradiction

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

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A32, A46, A51, A52, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

now :: thesis: contradiction

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 A31, A32, A33, A48, A53, GLIB_001:def 28; :: thesis: verum

end;

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

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

end;

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

hence contradiction by A32, A35, A45, A48, A53, 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;

A54: now :: thesis: ( P . (n + 1) DJoins v,P . (n + 2),G implies not P . (n + 1) DJoins P . (n + 2),v,G )

A55: n + 2 <= len P by A34, GLIB_001:1;
A56: n + 0 < n + 2 by XREAL_1:8;
assume that
A57: P . (n + 1) DJoins v,P . (n + 2),G and
A58: P . (n + 1) DJoins P . (n + 2),v,G ; :: thesis: contradiction
P . n = (the_Source_of G) . (P . (n + 1)) by A32, A57
.= P . (n + 2) by A58 ;
hence contradiction by A35, A56, A55, GLIB_001:def 28; :: thesis: verum

end;

n2 < n - 0 by XREAL_1:15;
then A59: n2 + 1 < n + 1 by XREAL_1:8;
n + 1 <= len P by A34, NAT_1:13;
then A60: P . (n2 + 1) <> P . (n + 1) by A39, A59, GLIB_001:138;

A61: now :: thesis: P . n2 <> v

n2 < n - 0 by XREAL_1:15;
hence P . n2 <> v by A31, A32, A33, GLIB_001:def 28; :: thesis: verum

end;

A62: ( not P . (n2 + 1) DJoins P . n2,v,G or not P . (n2 + 1) DJoins v,P . n2,G ) by A61;
A63: n2 < (len P) - 0 by A31, XREAL_1:15;
then A64: P . (n2 + 1) Joins P . n2,P . (n2 + 2),G by GLIB_001:def 3;
A65: P . (n + 1) Joins v,P . (n + 2),G by A32, A34, GLIB_001:def 3;

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

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 A32, A64, A65;

suppose A66: ( 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)));
A67: P . (n2 + 1) in v .edgesIn() by A66, GLIB_000:57;
dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) = {(P . (n2 + 1))} ;
then A69: 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 2
.= v .edgesIn() by A67, ZFMISC_1:40 ;
then reconsider XIN = (EL | (v .edgesIn())) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) as Rbag of v .edgesIn() by PARTFUN1:def 2, RELAT_1:def 18;

A70: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) holds
((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN . e

let e be object ; :: 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 A71: e in v .edgesIn() ;
then A72: (the_Target_of G) . e = v by GLIB_000:56;

now :: thesis: XIN . e = (FF:PushFlow (EL,P)) . e

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

suppose A73: 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 TARSKI:def 1;
hence XIN . e = ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) . (P . (n2 + 1)) by A73, FUNCT_4:13
.= (EL . (P . (n2 + 1))) + (P .tolerance EL) by FUNCOP_1:72
.= (FF:PushFlow (EL,P)) . e by A4, A63, A40, A66, A73, Def17 ;
:: thesis: verum

end;

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

A75: now :: thesis: not e in P .edges()

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

now :: thesis: contradiction

per cases ( v = v1 or v = v2 ) by A72, A80;

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

now :: thesis: contradiction

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

suppose m < n ; :: thesis: contradiction

hence contradiction by A31, A32, A33, A77, A82, GLIB_001:def 28; :: thesis: verum

end;

suppose A83: m = n ; :: thesis: contradiction

A84: (n + 2) - 2 < (n + 2) - 0 by XREAL_1:15;
A85: n + 2 <= len P by A34, GLIB_001:1;
P . (n + 2) = P . n by A32, A66, A72, A78, A83;
hence contradiction by A35, A84, A85, GLIB_001:def 28; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A32, A77, A81, A82, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

now :: thesis: contradiction

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 A31, A32, A33, A79, A86, GLIB_001:def 28; :: thesis: verum

end;

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

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

end;

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

hence contradiction by A32, A35, A76, A79, A86, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by A74, TARSKI:def 1;
then XIN . e = (EL | (v .edgesIn())) . e by FUNCT_4:11
.= EL . e by A71, FUNCT_1:49 ;
hence (FF:PushFlow (EL,P)) . e = XIN . e by A4, A71, A75, Def17; :: thesis: verum

end;

end;

end;

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

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
then A87: Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum XIN by A69, A70, FUNCT_1:2;
A88: dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
set XOUT = (EL | (v .edgesOut())) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL)));
A89: P . (n + 1) in v .edgesOut() by A66, GLIB_000:59;
dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) = {(P . (n + 1))} ;
then A91: 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 2
.= v .edgesOut() by A89, ZFMISC_1:40 ;
then reconsider XOUT = (EL | (v .edgesOut())) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) as Rbag of v .edgesOut() by PARTFUN1:def 2, RELAT_1:def 18;

A92: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) holds
((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT . e

let e be object ; :: 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 A93: e in v .edgesOut() ;
then A94: (the_Source_of G) . e = v by GLIB_000:58;

now :: thesis: XOUT . e = (FF:PushFlow (EL,P)) . e

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

suppose A95: 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 TARSKI:def 1;
hence XOUT . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) . (P . (n + 1)) by A95, FUNCT_4:13
.= (EL . (P . (n + 1))) + (P .tolerance EL) by FUNCOP_1:72
.= (FF:PushFlow (EL,P)) . e by A4, A32, A34, A66, A95, Def17 ;
:: thesis: verum

end;

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

A97: now :: thesis: not e in P .edges()

assume e in P .edges() ; :: thesis: contradiction
then consider v1, v2 being Vertex of G, m being odd Element of NAT such that
A98: m + 2 <= len P and
A99: v1 = P . m and
A100: e = P . (m + 1) and
A101: v2 = P . (m + 2) and
A102: e Joins v1,v2,G by GLIB_001:103;
A103: (m + 2) - 2 < (len P) - 0 by A98, XREAL_1:15;

now :: thesis: contradiction

per cases ( v = v1 or v = v2 ) by A94, A102;

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

now :: thesis: contradiction

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

suppose m < n ; :: thesis: contradiction

hence contradiction by A31, A32, A33, A99, A104, GLIB_001:def 28; :: thesis: verum

end;

suppose m = n ; :: thesis: contradiction

hence contradiction by A96, A100; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A32, A99, A103, A104, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

now :: thesis: contradiction

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 A31, A32, A33, A101, A105, GLIB_001:def 28; :: thesis: verum

end;

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

A107: n2 < n - 0 by XREAL_1:15;
P . n2 = P . n by A32, A66, A94, A100, A106;
hence contradiction by A31, A33, A107, GLIB_001:def 28; :: thesis: verum

end;

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

hence contradiction by A32, A35, A98, A101, A105, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A96, TARSKI:def 1;
then XOUT . e = (EL | (v .edgesOut())) . e by FUNCT_4:11
.= EL . e by A93, FUNCT_1:49 ;
hence (FF:PushFlow (EL,P)) . e = XOUT . e by A4, A93, A97, Def17; :: thesis: verum

end;

end;

end;

hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT . e by A93, FUNCT_1:49; :: 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 A30, A67, FUNCT_1:49
.= (((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 A89, FUNCT_1:49
.= Sum XOUT by GLIB_004:9 ;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A91, A87, A88, A92, FUNCT_1:2; :: thesis: verum

end;

suppose A108: ( 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()))

A109: dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;

A110: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) holds
((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (EL | (v .edgesOut())) . e

let e be object ; :: thesis: ( e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) implies ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (EL | (v .edgesOut())) . e )
assume A111: e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (EL | (v .edgesOut())) . e
then A112: (EL | (v .edgesOut())) . e = EL . e by FUNCT_1:49;
A113: e in v .edgesOut() by A111;
then A114: (the_Source_of G) . e = v by GLIB_000:58;
then A115: e <> P . (n + 1) by A36, A108;
e <> P . (n2 + 1) by A61, A108, A114;
then A116: not e in P .edges() by A41, A113, A115;
((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (FF:PushFlow (EL,P)) . e by A111, FUNCT_1:49;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (EL | (v .edgesOut())) . e by A4, A113, A112, A116, Def17; :: thesis: verum

end;

dom (EL | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
then A117: (FF:PushFlow (EL,P)) | (v .edgesOut()) = EL | (v .edgesOut()) by A109, A110, FUNCT_1:2;
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)));
A118: dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
A119: P . (n + 1) in v .edgesIn() by A108, GLIB_000:57;
A120: P . (n2 + 1) in v .edgesIn() by A108, GLIB_000:57;
A121: (FF:PushFlow (EL,P)) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) + (P .tolerance EL) by A4, A63, A40, A108, Def17;
A123: 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))}
.= (v .edgesIn()) \/ {(P . (n2 + 1))} by PARTFUN1:def 2
.= v .edgesIn() by A120, ZFMISC_1:40 ;
then reconsider XIN1 = (EL | (v .edgesIn())) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) as Rbag of v .edgesIn() by PARTFUN1:def 2, RELAT_1:def 18;
A124: 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 A123
.= v .edgesIn() by A119, ZFMISC_1:40 ;
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 v .edgesIn() by PARTFUN1:def 2, RELAT_1:def 18;
A126: (FF:PushFlow (EL,P)) . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) by A4, A32, A34, A54, A108, Def17;

A127: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) holds
((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e

let e be object ; :: thesis: ( e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) implies ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e )
assume A128: e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e
then A129: e in v .edgesIn() ;
A130: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (FF:PushFlow (EL,P)) . e by A128, FUNCT_1:49;

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

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

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

then A132: e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by TARSKI:def 1;
not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) by A60, A131, TARSKI:def 1;
then XIN2 . e = XIN1 . e by FUNCT_4:11
.= ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) . e by A132, FUNCT_4:13
.= (FF:PushFlow (EL,P)) . e by A121, A131, FUNCOP_1:72 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e by A128, FUNCT_1:49; :: thesis: verum

end;

suppose A133: 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 TARSKI:def 1;
then XIN2 . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) . (P . (n + 1)) by A133, FUNCT_4:13
.= (FF:PushFlow (EL,P)) . e by A126, A133, FUNCOP_1:72 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e by A128, FUNCT_1:49; :: thesis: verum

end;

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

then A135: not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by TARSKI:def 1;
A136: not e in P .edges() by A41, A129, A134;
not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) by A134, TARSKI:def 1;
then XIN2 . e = XIN1 . e by FUNCT_4:11
.= (EL | (v .edgesIn())) . e by A135, FUNCT_4:11
.= EL . e by A129, FUNCT_1:49 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e by A4, A129, A130, A136, Def17; :: 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 A60, TARSKI:def 1;
then XIN1 . (P . (n + 1)) = (EL | (v .edgesIn())) . (P . (n + 1)) by FUNCT_4:11
.= EL . (P . (n + 1)) by A119, FUNCT_1:49 ;
then Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = ((Sum XIN1) + ((EL . (P . (n + 1))) - (P .tolerance EL))) - (EL . (P . (n + 1))) by A124, A118, A127, FUNCT_1:2, 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 A120, FUNCT_1:49
.= Sum (EL | (v .edgesIn())) ;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A2, A28, A29, A117; :: thesis: verum

end;

suppose A137: ( 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()))

A138: dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;

A139: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) holds
((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (EL | (v .edgesIn())) . e

let e be object ; :: thesis: ( e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) implies ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (EL | (v .edgesIn())) . e )
assume A140: e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (EL | (v .edgesIn())) . e
then A141: (EL | (v .edgesIn())) . e = EL . e by FUNCT_1:49;
A142: e in v .edgesIn() by A140;
then A143: (the_Target_of G) . e = v by GLIB_000:56;
then A144: e <> P . (n + 1) by A36, A137;
e <> P . (n2 + 1) by A61, A137, A143;
then A145: not e in P .edges() by A41, A142, A144;
((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (FF:PushFlow (EL,P)) . e by A140, FUNCT_1:49;
hence ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (EL | (v .edgesIn())) . e by A4, A142, A141, A145, Def17; :: thesis: verum

end;

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)));
A146: dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
A147: P . (n + 1) in v .edgesOut() by A137, GLIB_000:59;
A148: dom (EL | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
A149: P . (n2 + 1) in v .edgesOut() by A137, GLIB_000:59;
A150: (FF:PushFlow (EL,P)) . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) by A4, A32, A34, A137, Def17;
A152: 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))}
.= (v .edgesOut()) \/ {(P . (n2 + 1))} by PARTFUN1:def 2
.= v .edgesOut() by A149, ZFMISC_1:40 ;
then reconsider XOUT1 = (EL | (v .edgesOut())) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) as Rbag of v .edgesOut() by PARTFUN1:def 2, RELAT_1:def 18;
A153: 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 A152
.= v .edgesOut() by A147, ZFMISC_1:40 ;
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 v .edgesOut() by PARTFUN1:def 2, RELAT_1:def 18;
A155: (FF:PushFlow (EL,P)) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) - (P .tolerance EL) by A4, A63, A40, A62, A137, Def17;

A156: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) holds
((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e

let e be object ; :: thesis: ( e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) implies ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e )
assume A157: e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e
then A158: e in v .edgesOut() ;
A159: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (FF:PushFlow (EL,P)) . e by A157, FUNCT_1:49;

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

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

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

then A161: e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) by TARSKI:def 1;
not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A60, A160, TARSKI:def 1;
then XOUT2 . e = XOUT1 . e by FUNCT_4:11
.= ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) . e by A161, FUNCT_4:13
.= (FF:PushFlow (EL,P)) . e by A155, A160, FUNCOP_1:72 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e by A157, FUNCT_1:49; :: thesis: verum

end;

suppose A162: 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 TARSKI:def 1;
then XOUT2 . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) . e by FUNCT_4:13
.= (FF:PushFlow (EL,P)) . e by A150, A162, FUNCOP_1:72 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e by A157, FUNCT_1:49; :: thesis: verum

end;

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

then A164: not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) by TARSKI:def 1;
A165: not e in P .edges() by A41, A158, A163;
not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A163, TARSKI:def 1;
then XOUT2 . e = XOUT1 . e by FUNCT_4:11
.= (EL | (v .edgesOut())) . e by A164, FUNCT_4:11
.= EL . e by A158, FUNCT_1:49 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e by A4, A158, A159, A165, Def17; :: 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 A60, TARSKI:def 1;
then XOUT1 . (P . (n + 1)) = (EL | (v .edgesOut())) . (P . (n + 1)) by FUNCT_4:11
.= EL . (P . (n + 1)) by A147, FUNCT_1:49 ;
then Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) = ((Sum XOUT1) + ((EL . (P . (n + 1))) + (P .tolerance EL))) - (EL . (P . (n + 1))) by A153, A146, A156, FUNCT_1:2, 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 A149, FUNCT_1:49
.= Sum (EL | (v .edgesOut())) ;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A30, A138, A148, A139, FUNCT_1:2; :: thesis: verum

end;

suppose A166: ( 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()))

set XIN = (EL | (v .edgesIn())) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL)));
A167: P . (n + 1) in v .edgesIn() by A166, GLIB_000:57;
dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) = {(P . (n + 1))} ;
then A169: 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 2
.= v .edgesIn() by A167, ZFMISC_1:40 ;
then reconsider XIN = (EL | (v .edgesIn())) +* ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) as Rbag of v .edgesIn() by PARTFUN1:def 2, RELAT_1:def 18;
A170: (FF:PushFlow (EL,P)) . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) by A4, A32, A34, A54, A166, Def17;

A171: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) holds
XIN . e = ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e

let e be object ; :: 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 A172: e in v .edgesIn() ;
then A173: (the_Target_of G) . e = v by GLIB_000:56;

now :: thesis: XIN . e = (FF:PushFlow (EL,P)) . e

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

suppose A174: 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 TARSKI:def 1;
hence XIN . e = ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) . (P . (n + 1)) by A174, FUNCT_4:13
.= (FF:PushFlow (EL,P)) . e by A170, A174, FUNCOP_1:72 ;
:: thesis: verum

end;

suppose A175: 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 TARSKI:def 1;
then A176: XIN . e = (EL | (v .edgesIn())) . e by FUNCT_4:11
.= EL . e by A172, FUNCT_1:49 ;
e <> P . (n2 + 1) by A61, A166, A173;
then not e in P .edges() by A41, A172, A175;
hence (FF:PushFlow (EL,P)) . e = XIN . e by A4, A172, A176, Def17; :: thesis: verum

end;

end;

end;

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

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
then A177: 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 A169, A171, FUNCT_1:2, GLIB_004:9
.= (((Sum (EL | (v .edgesIn()))) + (EL . (P . (n + 1)))) - (P .tolerance EL)) - (EL . (P . (n + 1))) by A167, FUNCT_1:49
.= (Sum (EL | (v .edgesIn()))) - (P .tolerance EL) ;
set XOUT = (EL | (v .edgesOut())) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)));
A178: P . (n2 + 1) in v .edgesOut() by A166, GLIB_000:59;
dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) = {(P . (n2 + 1))} ;
then A180: dom ((EL | (v .edgesOut())) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL)))) = (dom (EL | (v .edgesOut()))) \/ {(P . (n2 + 1))} by FUNCT_4:def 1
.= (v .edgesOut()) \/ {(P . (n2 + 1))} by PARTFUN1:def 2
.= v .edgesOut() by A178, ZFMISC_1:40 ;
then reconsider XOUT = (EL | (v .edgesOut())) +* ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) as Rbag of v .edgesOut() by PARTFUN1:def 2, RELAT_1:def 18;
A181: (FF:PushFlow (EL,P)) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) - (P .tolerance EL) by A4, A63, A40, A62, A166, Def17;

A182: now :: thesis: for e being object st e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) holds
XOUT . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e

let e be object ; :: 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 A183: e in v .edgesOut() ;
then A184: (the_Source_of G) . e = v by GLIB_000:58;

now :: thesis: XOUT . e = (FF:PushFlow (EL,P)) . e

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

suppose A185: 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 TARSKI:def 1;
hence XOUT . e = ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) . (P . (n2 + 1)) by A185, FUNCT_4:13
.= (FF:PushFlow (EL,P)) . e by A181, A185, FUNCOP_1:72 ;
:: thesis: verum

end;

suppose A186: 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 TARSKI:def 1;
then A187: XOUT . e = (EL | (v .edgesOut())) . e by FUNCT_4:11
.= EL . e by A183, FUNCT_1:49 ;
e <> P . (n + 1) by A36, A166, A184;
then not e in P .edges() by A41, A183, A186;
hence (FF:PushFlow (EL,P)) . e = XOUT . e by A4, A183, A187, Def17; :: thesis: verum

end;

end;

end;

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

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
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 A180, A182, FUNCT_1:2, GLIB_004:9
.= (((Sum (EL | (v .edgesOut()))) + (EL . (P . (n2 + 1)))) - (P .tolerance EL)) - (EL . (P . (n2 + 1))) by A178, FUNCT_1:49
.= (Sum (EL | (v .edgesIn()))) - (P .tolerance EL) by A30 ;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A177; :: thesis: verum

end;

end;

end;

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

end;

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

A189: dom (EL | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;

A190: now :: thesis: for e being object st e in dom (EL | (v .edgesOut())) holds
(EL | (v .edgesOut())) . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e

let e be object ; :: thesis: ( e in dom (EL | (v .edgesOut())) implies (EL | (v .edgesOut())) . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e )
assume A191: e in dom (EL | (v .edgesOut())) ; :: thesis: (EL | (v .edgesOut())) . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e
then A192: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (FF:PushFlow (EL,P)) . e by FUNCT_1:49;
A193: e in v .edgesOut() by A191;

A194: now :: thesis: not e in P .edges()

consider x being set such that
A195: e DJoins v,x,G by A193, GLIB_000:59;
assume A196: e in P .edges() ; :: thesis: contradiction
e Joins v,x,G by A195;
hence contradiction by A188, A196, GLIB_001:105; :: thesis: verum

end;

(EL | (v .edgesOut())) . e = EL . e by A191, FUNCT_1:49;
hence (EL | (v .edgesOut())) . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e by A4, A193, A192, A194, Def17; :: thesis: verum

end;

A197: dom (EL | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;

A198: now :: thesis: for e being object st e in dom (EL | (v .edgesIn())) holds
(EL | (v .edgesIn())) . e = ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e

let e be object ; :: thesis: ( e in dom (EL | (v .edgesIn())) implies (EL | (v .edgesIn())) . e = ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e )
assume A199: e in dom (EL | (v .edgesIn())) ; :: thesis: (EL | (v .edgesIn())) . e = ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e
then A200: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (FF:PushFlow (EL,P)) . e by FUNCT_1:49;

A201: now :: thesis: not e in P .edges()

consider x being set such that
A202: e DJoins x,v,G by A199, GLIB_000:57;
assume A203: e in P .edges() ; :: thesis: contradiction
e Joins x,v,G by A202;
hence contradiction by A188, A203, GLIB_001:105; :: thesis: verum

end;

(EL | (v .edgesIn())) . e = EL . e by A199, FUNCT_1:49;
hence (EL | (v .edgesIn())) . e = ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e by A4, A197, A199, A200, A201, Def17; :: thesis: verum

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
then A204: EL | (v .edgesOut()) = (FF:PushFlow (EL,P)) | (v .edgesOut()) by A189, A190, FUNCT_1:2;
dom (EL | (v .edgesIn())) = dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) by A197, PARTFUN1:def 2;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum (EL | (v .edgesIn())) by A198, FUNCT_1:2
.= Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A2, A28, A29, A204 ;
:: 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 ; :: thesis: verum