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

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

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 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

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, GLIB_000:def 14;
A16: (the_Source_of G) . e = P . (n + 2) by A14, GLIB_000:def 14;
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: not 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

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

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, Def2;

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

A33: now

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

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

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

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

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

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, GLIB_000:def 13; :: 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, GLIB_000:def 13; :: thesis: verum

end;

end;

end;

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

now

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

suppose A52: 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 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

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

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, GLIB_000:def 14
.= P . (n + 2) by A58, GLIB_000:def 14 ;
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

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

end;

A63: now

assume that
A64: P . (n2 + 1) DJoins P . n2,v,G and
A65: P . (n2 + 1) DJoins v,P . n2,G ; :: thesis: contradiction
P . n2 = (the_Source_of G) . (P . (n2 + 1)) by A64, GLIB_000:def 14
.= v by A65, GLIB_000:def 14 ;
hence contradiction by A61; :: thesis: verum

end;

A66: n2 < (len P) - 0 by A31, XREAL_1:15;
then A67: P . (n2 + 1) Joins P . n2,P . (n2 + 2),G by GLIB_001:def 3;
A68: P . (n + 1) Joins v,P . (n + 2),G by A32, A34, GLIB_001:def 3;

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 A32, A67, A68, GLIB_000:16;

suppose A69: ( 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)));
A70: P . (n2 + 1) in v .edgesIn() by A69, GLIB_000:57;
A71: dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) = {(P . (n2 + 1))} by FUNCOP_1:13;
then A72: 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 A70, 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;

A73: 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 A74: e in v .edgesIn() by PARTFUN1:def 2;
then A75: (the_Target_of G) . e = v by GLIB_000:56;

now

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

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

end;

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

A78: now

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

now

per cases ( v = v1 or v = v2 ) by A75, A83, GLIB_000:def 13;

suppose A85: 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 A31, A32, A33, A80, A85, GLIB_001:def 28; :: thesis: verum

end;

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

A87: (n + 2) - 2 < (n + 2) - 0 by XREAL_1:15;
A88: n + 2 <= len P by A34, GLIB_001:1;
P . (n + 2) = P . n by A32, A69, A75, A81, A86, GLIB_000:def 14;
hence contradiction by A35, A87, A88, GLIB_001:def 28; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A32, A80, A84, A85, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A89: 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 A31, A32, A33, A82, A89, GLIB_001:def 28; :: thesis: verum

end;

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

hence contradiction by A77, A81; :: thesis: verum

end;

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

hence contradiction by A32, A35, A79, A82, A89, 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 A71, A77, TARSKI:def 1;
then XIN . e = (EL | (v .edgesIn())) . e by FUNCT_4:11
.= EL . e by A74, FUNCT_1:49 ;
hence (FF:PushFlow (EL,P)) . e = XIN . e by A4, A74, A78, Def17; :: thesis: verum

end;

end;

end;

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

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
then A90: Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum XIN by A72, A73, FUNCT_1:2;
A91: 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)));
A92: P . (n + 1) in v .edgesOut() by A69, GLIB_000:59;
A93: dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) = {(P . (n + 1))} by FUNCOP_1:13;
then A94: 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 A92, 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;

A95: 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 A96: e in v .edgesOut() by PARTFUN1:def 2;
then A97: (the_Source_of G) . e = v by GLIB_000:58;

now

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

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

end;

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

A100: now

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

now

per cases ( v = v1 or v = v2 ) by A97, A105, GLIB_000:def 13;

suppose A107: 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 A31, A32, A33, A102, A107, GLIB_001:def 28; :: thesis: verum

end;

suppose m = n ; :: thesis: contradiction

hence contradiction by A99, A103; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

hence contradiction by A32, A102, A106, A107, GLIB_001:def 28; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A108: 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 A31, A32, A33, A104, A108, GLIB_001:def 28; :: thesis: verum

end;

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

A110: n2 < n - 0 by XREAL_1:15;
P . n2 = P . n by A32, A69, A97, A103, A109, GLIB_000:def 14;
hence contradiction by A31, A33, A110, GLIB_001:def 28; :: thesis: verum

end;

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

hence contradiction by A32, A35, A101, A104, A108, 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 A93, A99, TARSKI:def 1;
then XOUT . e = (EL | (v .edgesOut())) . e by FUNCT_4:11
.= EL . e by A96, FUNCT_1:49 ;
hence (FF:PushFlow (EL,P)) . e = XOUT . e by A4, A96, A100, Def17; :: thesis: verum

end;

end;

end;

hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT . e by A96, 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, A70, 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 A92, 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 A94, A90, A91, A95, FUNCT_1:2; :: thesis: verum

end;

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

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

A113: 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 A114: e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (EL | (v .edgesOut())) . e
then A115: (EL | (v .edgesOut())) . e = EL . e by A112, FUNCT_1:49;
A116: e in v .edgesOut() by A114, PARTFUN1:def 2;
then A117: (the_Source_of G) . e = v by GLIB_000:58;
then A118: e <> P . (n + 1) by A36, A111, GLIB_000:def 14;
e <> P . (n2 + 1) by A61, A111, A117, GLIB_000:def 14;
then A119: not e in P .edges() by A41, A116, A118;
((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (FF:PushFlow (EL,P)) . e by A112, A114, FUNCT_1:49;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (EL | (v .edgesOut())) . e by A4, A116, A115, A119, Def17; :: thesis: verum

end;

dom (EL | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
then A120: (FF:PushFlow (EL,P)) | (v .edgesOut()) = EL | (v .edgesOut()) by A112, A113, 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)));
A121: dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
A122: P . (n + 1) in v .edgesIn() by A111, GLIB_000:57;
A123: P . (n2 + 1) in v .edgesIn() by A111, GLIB_000:57;
A124: (FF:PushFlow (EL,P)) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) + (P .tolerance EL) by A4, A66, A40, A111, Def17;
A125: dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) = {(P . (n + 1))} by FUNCOP_1:13;
A126: 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:13
.= (v .edgesIn()) \/ {(P . (n2 + 1))} by PARTFUN1:def 2
.= v .edgesIn() by A123, 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;
A127: 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 A126, FUNCOP_1:13
.= v .edgesIn() by A122, 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;
A128: dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) = {(P . (n2 + 1))} by FUNCOP_1:13;
A129: (FF:PushFlow (EL,P)) . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) by A4, A32, A34, A54, A111, Def17;

A130: 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 A131: e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e
then A132: e in v .edgesIn() by PARTFUN1:def 2;
A133: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (FF:PushFlow (EL,P)) . e by A121, A131, FUNCT_1:49;

now

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

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

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

end;

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

end;

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

then A138: not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) + (P .tolerance EL))) by A128, TARSKI:def 1;
A139: not e in P .edges() by A41, A132, A137;
not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) by A125, A137, TARSKI:def 1;
then XIN2 . e = XIN1 . e by FUNCT_4:11
.= (EL | (v .edgesIn())) . e by A138, FUNCT_4:11
.= EL . e by A132, FUNCT_1:49 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = XIN2 . e by A4, A132, A133, A139, 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, A128, TARSKI:def 1;
then XIN1 . (P . (n + 1)) = (EL | (v .edgesIn())) . (P . (n + 1)) by FUNCT_4:11
.= EL . (P . (n + 1)) by A122, 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 A127, A121, A130, 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 A123, 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, A120, Def2; :: thesis: verum

end;

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

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

A142: 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 A143: e in dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (EL | (v .edgesIn())) . e
then A144: (EL | (v .edgesIn())) . e = EL . e by A141, FUNCT_1:49;
A145: e in v .edgesIn() by A143, PARTFUN1:def 2;
then A146: (the_Target_of G) . e = v by GLIB_000:56;
then A147: e <> P . (n + 1) by A36, A140, GLIB_000:def 14;
e <> P . (n2 + 1) by A61, A140, A146, GLIB_000:def 14;
then A148: not e in P .edges() by A41, A145, A147;
((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (FF:PushFlow (EL,P)) . e by A141, A143, FUNCT_1:49;
hence ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (EL | (v .edgesIn())) . e by A4, A145, A144, A148, 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)));
A149: dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
A150: P . (n + 1) in v .edgesOut() by A140, GLIB_000:59;
A151: dom (EL | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
A152: P . (n2 + 1) in v .edgesOut() by A140, GLIB_000:59;
A153: (FF:PushFlow (EL,P)) . (P . (n + 1)) = (EL . (P . (n + 1))) + (P .tolerance EL) by A4, A32, A34, A140, Def17;
A154: dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) = {(P . (n + 1))} by FUNCOP_1:13;
A155: 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:13
.= (v .edgesOut()) \/ {(P . (n2 + 1))} by PARTFUN1:def 2
.= v .edgesOut() by A152, 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;
A156: 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 A155, FUNCOP_1:13
.= v .edgesOut() by A150, 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;
A157: dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) = {(P . (n2 + 1))} by FUNCOP_1:13;
A158: (FF:PushFlow (EL,P)) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) - (P .tolerance EL) by A4, A66, A40, A63, A140, Def17;

A159: 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 A160: e in dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) ; :: thesis: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e
then A161: e in v .edgesOut() by PARTFUN1:def 2;
A162: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (FF:PushFlow (EL,P)) . e by A149, A160, FUNCT_1:49;

now

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

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

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

end;

suppose A165: 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 A154, 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 A153, A165, FUNCOP_1:72 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e by A149, A160, FUNCT_1:49; :: thesis: verum

end;

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

then A167: not e in dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) by A157, TARSKI:def 1;
A168: not e in P .edges() by A41, A161, A166;
not e in dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) + (P .tolerance EL))) by A154, A166, TARSKI:def 1;
then XOUT2 . e = XOUT1 . e by FUNCT_4:11
.= (EL | (v .edgesOut())) . e by A167, FUNCT_4:11
.= EL . e by A161, FUNCT_1:49 ;
hence ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = XOUT2 . e by A4, A161, A162, A168, 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, A157, TARSKI:def 1;
then XOUT1 . (P . (n + 1)) = (EL | (v .edgesOut())) . (P . (n + 1)) by FUNCT_4:11
.= EL . (P . (n + 1)) by A150, 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 A156, A149, A159, 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 A152, FUNCT_1:49
.= Sum (EL | (v .edgesOut())) ;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A30, A141, A151, A142, FUNCT_1:2; :: thesis: verum

end;

suppose A169: ( 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)));
A170: P . (n + 1) in v .edgesIn() by A169, GLIB_000:57;
A171: dom ((P . (n + 1)) .--> ((EL . (P . (n + 1))) - (P .tolerance EL))) = {(P . (n + 1))} by FUNCOP_1:13;
then A172: 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 A170, 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;
A173: (FF:PushFlow (EL,P)) . (P . (n + 1)) = (EL . (P . (n + 1))) - (P .tolerance EL) by A4, A32, A34, A54, A169, Def17;

A174: 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 A175: e in v .edgesIn() by PARTFUN1:def 2;
then A176: (the_Target_of G) . e = v by GLIB_000:56;

now

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

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

end;

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

end;

end;

end;

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

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) = v .edgesIn() by PARTFUN1:def 2;
then A180: 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 A172, A174, FUNCT_1:2, GLIB_004:9
.= (((Sum (EL | (v .edgesIn()))) + (EL . (P . (n + 1)))) - (P .tolerance EL)) - (EL . (P . (n + 1))) by A170, 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)));
A181: P . (n2 + 1) in v .edgesOut() by A169, GLIB_000:59;
A182: dom ((P . (n2 + 1)) .--> ((EL . (P . (n2 + 1))) - (P .tolerance EL))) = {(P . (n2 + 1))} by FUNCOP_1:13;
then A183: 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 A181, 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;
A184: (FF:PushFlow (EL,P)) . (P . (n2 + 1)) = (EL . (P . (n2 + 1))) - (P .tolerance EL) by A4, A66, A40, A63, A169, Def17;

A185: 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 A186: e in v .edgesOut() by PARTFUN1:def 2;
then A187: (the_Source_of G) . e = v by GLIB_000:58;

now

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

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

end;

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

end;

end;

end;

hence XOUT . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e by A186, 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 A183, A185, FUNCT_1:2, GLIB_004:9
.= (((Sum (EL | (v .edgesOut()))) + (EL . (P . (n2 + 1)))) - (P .tolerance EL)) - (EL . (P . (n2 + 1))) by A181, 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 A180; :: thesis: verum

end;

end;

end;

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

end;

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

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

A193: 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 A194: e in dom (EL | (v .edgesOut())) ; :: thesis: (EL | (v .edgesOut())) . e = ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e
then A195: ((FF:PushFlow (EL,P)) | (v .edgesOut())) . e = (FF:PushFlow (EL,P)) . e by A192, FUNCT_1:49;
A196: e in v .edgesOut() by A194, PARTFUN1:def 2;

A197: now

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

end;

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

end;

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

A201: 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 A202: e in dom (EL | (v .edgesIn())) ; :: thesis: (EL | (v .edgesIn())) . e = ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e
then A203: ((FF:PushFlow (EL,P)) | (v .edgesIn())) . e = (FF:PushFlow (EL,P)) . e by A200, FUNCT_1:49;

A204: now

consider x being set such that
A205: e DJoins x,v,G by A200, A202, GLIB_000:57;
assume A206: e in P .edges() ; :: thesis: contradiction
e Joins x,v,G by A205, GLIB_000:16;
hence contradiction by A191, A206, GLIB_001:105; :: thesis: verum

end;

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

end;

dom ((FF:PushFlow (EL,P)) | (v .edgesOut())) = v .edgesOut() by PARTFUN1:def 2;
then A207: EL | (v .edgesOut()) = (FF:PushFlow (EL,P)) | (v .edgesOut()) by A192, A193, FUNCT_1:2;
dom (EL | (v .edgesIn())) = dom ((FF:PushFlow (EL,P)) | (v .edgesIn())) by A200, PARTFUN1:def 2;
hence Sum ((FF:PushFlow (EL,P)) | (v .edgesIn())) = Sum (EL | (v .edgesIn())) by A201, FUNCT_1:2
.= Sum ((FF:PushFlow (EL,P)) | (v .edgesOut())) by A2, A28, A29, A207, Def2 ;
:: 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 Def2; :: thesis: verum