let G be finite real-weighted WGraph; :: thesis:
let EL be FF:ELabeling of G; :: thesis:
let source, sink be set ; :: thesis:
let V be Subset of (the_Vertices_of G); :: thesis:
assume that
A1: EL has_valid_flow_from source,sink and
A2: source in V and
A3: not sink in V ; :: thesis:
set VG = the_Vertices_of G;
set n = card ((the_Vertices_of G) \ V);

A4: now

assume card ((the_Vertices_of G) \ V) = 0 ; :: thesis:
then A5: (the_Vertices_of G) \ V = {} ;
sink is Vertex of G by A1, Def2;
hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis:

end;

defpred S₁[ Nat] means for V being Subset of (the_Vertices_of G) st card ((the_Vertices_of G) \ V) = $1 & source in V & not sink in V holds
EL .flow source,sink = (Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V)));
set TG = the_Target_of G;
set SG = the_Source_of G;

A6: now

let n be non empty Nat; :: thesis:
assume A7: S₁[n] ; :: thesis:

now

now

end;

now

end;

then A25: G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) c= G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) by TARSKI:def 3;

now

end;

A30: now

let e be set ; :: thesis:
assume e in dom (EL | EA) ; :: thesis:
then A31: e in EA by PARTFUN1:def 4;

now

per cases ;

suppose not e in G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then A32: e in EB by A31, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EB)) . e = (EL | EB) . e by A29, FUNCT_4:14
.= EL . e by A32, FUNCT_1:72 ;
:: thesis:

end;

suppose A33: e in G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then not e in EB by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EB)) . e = (EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) . e by A29, FUNCT_4:12
.= EL . e by A33, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | EA) . e = ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EB)) . e by A31, FUNCT_1:72; :: thesis:

end;

now

let e be set ; :: thesis:

hereby :: thesis:

end;

end;

then A45: (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) \ (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2) = G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) by TARSKI:2;
A46: dom (EL | ED) = ED by PARTFUN1:def 4;

A47: now

let e be set ; :: thesis:
assume e in dom (EL | EC) ; :: thesis:
then A48: e in EC by PARTFUN1:def 4;

now

per cases ;

suppose not e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 ; :: thesis:

then A49: e in ED by A48, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | ED)) . e = (EL | ED) . e by A46, FUNCT_4:14
.= EL . e by A49, FUNCT_1:72 ;
:: thesis:

end;

suppose A50: e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 ; :: thesis:

then not e in ED by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | ED)) . e = (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) . e by A46, FUNCT_4:12
.= EL . e by A50, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | EC) . e = ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | ED)) . e by A48, FUNCT_1:72; :: thesis:

end;

reconsider EXV1cb = (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) \ (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2) as Subset of (the_Edges_of G) ;
set EXXf = G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))};
A51: dom (EL | EC) = EC by PARTFUN1:def 4;

now

let e be set ; :: thesis:

hereby :: thesis:

end;

end;

then A63: (G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))}) \ (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))}) = G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} by TARSKI:2;

now

end;

then A67: G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} c= G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),(V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by TARSKI:def 3;
A68: not choose (((the_Vertices_of G) \ V2) \ {sink}) in V2 by A12, XBOOLE_0:def 5;

now

end;

then A73: G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} c= G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} by TARSKI:def 3;
A74: V2 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} is Subset of V2 ;

now

hereby :: thesis:

assume A76: e in G .edgesDBetween V2,((the_Vertices_of G) \ V2) ; :: thesis:
then A77: e DSJoins V2,(the_Vertices_of G) \ V2,G by GLIB_000:def 33;
then A78: (the_Source_of G) . e in V2 by GLIB_000:def 18;

A79: now

assume e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) ; :: thesis:
then e DSJoins {(choose (((the_Vertices_of G) \ V2) \ {sink}))},(the_Vertices_of G) \ V1,G by GLIB_000:def 33;
then (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by GLIB_000:def 18;
hence contradiction by A68, A78, TARSKI:def 1; :: thesis:

end;

A80: (the_Target_of G) . e in (the_Vertices_of G) \ V2 by A77, GLIB_000:def 18;
A81: (the_Source_of G) . e in V1 by A78, XBOOLE_0:def 3;

now

per cases ) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} or not (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ) ;

suppose (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

end;

suppose not (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

end;

hence e in ((G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) \/ (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) \ (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) ; :: thesis:

end;

now

per cases by A82, A75, XBOOLE_0:def 3;

suppose A84: e in G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) ; :: thesis:

then A85: e DSJoins V1,(the_Vertices_of G) \ V1,G by GLIB_000:def 33;
then A86: (the_Source_of G) . e in V1 by GLIB_000:def 18;
A87: (the_Target_of G) . e in (the_Vertices_of G) \ V1 by A85, GLIB_000:def 18;
then not (the_Target_of G) . e in V1 by XBOOLE_0:def 5;
then not (the_Target_of G) . e in V2 by XBOOLE_0:def 3;
then A88: (the_Target_of G) . e in (the_Vertices_of G) \ V2 by A87, XBOOLE_0:def 5;
not (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A83, A84, A87, GLIB_000:def 18;
then (the_Source_of G) . e in V1 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A86, XBOOLE_0:def 5;
then (the_Source_of G) . e in V2 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by XBOOLE_1:40;
hence e DSJoins V2,(the_Vertices_of G) \ V2,G by A74, A84, A88, GLIB_000:def 18; :: thesis:

end;

suppose A89: e in G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then A90: e DSJoins V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))},G by GLIB_000:def 33;
then A91: (the_Source_of G) . e in V2 by GLIB_000:def 18;
(the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A90, GLIB_000:def 18;
then A92: not (the_Target_of G) . e in V2 by A68, TARSKI:def 1;
(the_Target_of G) . e in the_Vertices_of G by A89, FUNCT_2:7;
then (the_Target_of G) . e in (the_Vertices_of G) \ V2 by A92, XBOOLE_0:def 5;
hence e DSJoins V2,(the_Vertices_of G) \ V2,G by A89, A91, GLIB_000:def 18; :: thesis:

end;

hence e in G .edgesDBetween V2,((the_Vertices_of G) \ V2) by GLIB_000:def 33; :: thesis:

end;

then A93: G .edgesDBetween V2,((the_Vertices_of G) \ V2) = ((G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) \/ (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) \ (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) by TARSKI:2;

now

hereby :: thesis:

assume A95: e in G .edgesDBetween ((the_Vertices_of G) \ V2),V2 ; :: thesis:
then A96: e DSJoins (the_Vertices_of G) \ V2,V2,G by GLIB_000:def 33;
then A97: (the_Target_of G) . e in V2 by GLIB_000:def 18;

A98: now

assume e in G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:
then e DSJoins (the_Vertices_of G) \ V1,{(choose (((the_Vertices_of G) \ V2) \ {sink}))},G by GLIB_000:def 33;
then (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by GLIB_000:def 18;
hence contradiction by A68, A97, TARSKI:def 1; :: thesis:

end;

A99: (the_Source_of G) . e in (the_Vertices_of G) \ V2 by A96, GLIB_000:def 18;
A100: (the_Target_of G) . e in V1 by A97, XBOOLE_0:def 3;

now

per cases ) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} or not (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ) ;

suppose (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

end;

suppose not (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

end;

hence e in ((G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),(V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) \/ (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) \ (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))}) ; :: thesis:

end;

now

per cases by A101, A94, XBOOLE_0:def 3;

suppose A103: e in G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),(V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) ; :: thesis:

then A104: e DSJoins (the_Vertices_of G) \ V1,V1,G by GLIB_000:def 33;
then A105: (the_Target_of G) . e in V1 by GLIB_000:def 18;
A106: (the_Source_of G) . e in (the_Vertices_of G) \ V1 by A104, GLIB_000:def 18;
then not (the_Source_of G) . e in V1 by XBOOLE_0:def 5;
then not (the_Source_of G) . e in V2 by XBOOLE_0:def 3;
then A107: (the_Source_of G) . e in (the_Vertices_of G) \ V2 by A106, XBOOLE_0:def 5;
not (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A102, A103, A106, GLIB_000:def 18;
then (the_Target_of G) . e in V1 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A105, XBOOLE_0:def 5;
then (the_Target_of G) . e in V2 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by XBOOLE_1:40;
hence e DSJoins (the_Vertices_of G) \ V2,V2,G by A74, A103, A107, GLIB_000:def 18; :: thesis:

end;

suppose A108: e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 ; :: thesis:

then A109: e DSJoins {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2,G by GLIB_000:def 33;
then A110: (the_Target_of G) . e in V2 by GLIB_000:def 18;
(the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A109, GLIB_000:def 18;
then A111: not (the_Source_of G) . e in V2 by A68, TARSKI:def 1;
(the_Source_of G) . e in the_Vertices_of G by A108, FUNCT_2:7;
then (the_Source_of G) . e in (the_Vertices_of G) \ V2 by A111, XBOOLE_0:def 5;
hence e DSJoins (the_Vertices_of G) \ V2,V2,G by A108, A110, GLIB_000:def 18; :: thesis:

end;

hence e in G .edgesDBetween ((the_Vertices_of G) \ V2),V2 by GLIB_000:def 33; :: thesis:

end;

then A112: G .edgesDBetween ((the_Vertices_of G) \ V2),V2 = E2 by TARSKI:2;
A113: dom (EL | E2) = EC \ (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by PARTFUN1:def 4;

A114: now

let e be set ; :: thesis:
assume e in dom (EL | EC) ; :: thesis:
then A115: e in EC by PARTFUN1:def 4;

now

per cases ;

suppose not e in G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then A116: e in E2 by A115, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | E2)) . e = (EL | E2) . e by A113, FUNCT_4:14
.= EL . e by A116, FUNCT_1:72 ;
:: thesis:

end;

suppose A117: e in G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then not e in E2 by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | E2)) . e = (EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) . e by A113, FUNCT_4:12
.= EL . e by A117, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | EC) . e = ((EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | E2)) . e by A115, FUNCT_1:72; :: thesis:

end;

now

end;

then A126: G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 c= G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by TARSKI:def 3;
A127: dom (EL | E1) = EA \ (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) by PARTFUN1:def 4;

A128: now

let e be set ; :: thesis:
assume e in dom (EL | EA) ; :: thesis:
then A129: e in EA by PARTFUN1:def 4;

now

per cases ;

suppose not e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) ; :: thesis:

then A130: e in E1 by A129, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) +* (EL | E1)) . e = (EL | E1) . e by A127, FUNCT_4:14
.= EL . e by A130, FUNCT_1:72 ;
:: thesis:

end;

suppose A131: e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})) ; :: thesis:

then not e in E1 by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) +* (EL | E1)) . e = (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) . e by A127, FUNCT_4:12
.= EL . e by A131, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | EA) . e = ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) +* (EL | E1)) . e by A129, FUNCT_1:72; :: thesis:

end;

A132: dom (EL | (G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) = G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} by PARTFUN1:def 4;

A133: now

let e be set ; :: thesis:
assume A134: e in dom (EL | (G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) ; :: thesis:
then A135: e in G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} by PARTFUN1:def 4;

now

per cases ;

suppose A136: e in G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then not e in EV1Xdb by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EV1Xdb)) . e = (EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) . e by A121, FUNCT_4:12
.= EL . e by A136, FUNCT_1:72 ;
:: thesis:

end;

suppose not e in G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:

then A137: e in EV1Xdb by A135, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EV1Xdb)) . e = (EL | EV1Xdb) . e by A121, FUNCT_4:14
.= EL . e by A137, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | (G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) . e = ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EV1Xdb)) . e by A132, A134, FUNCT_1:72; :: thesis:

end;

A142: now

let e be set ; :: thesis:
assume A143: e in dom (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) ; :: thesis:
then A144: e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by PARTFUN1:def 4;

now

per cases ;

suppose A145: e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 ; :: thesis:

then not e in EXV1cb by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | EXV1cb)) . e = (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) . e by A140, FUNCT_4:12
.= EL . e by A145, FUNCT_1:72 ;
:: thesis:

end;

suppose not e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 ; :: thesis:

then A146: e in EXV1cb by A144, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | EXV1cb)) . e = (EL | EXV1cb) . e by A140, FUNCT_4:14
.= EL . e by A146, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) . e = ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | EXV1cb)) . e by A141, A143, FUNCT_1:72; :: thesis:

end;

now

let e be set ; :: thesis:

hereby :: thesis:

assume A150: e in (G .edgesDBetween (the_Vertices_of G),{x}) \ (G .edgesDBetween {x},{x}) ; :: thesis:
then e in G .edgesDBetween (the_Vertices_of G),{x} by XBOOLE_0:def 5;
then A151: e DSJoins the_Vertices_of G,{x},G by GLIB_000:def 33;
then A152: (the_Source_of G) . e in the_Vertices_of G by GLIB_000:def 18;
A153: (the_Target_of G) . e in {x} by A151, GLIB_000:def 18;
not e in G .edgesDBetween {x},{x} by A150, XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 33;
then not (the_Source_of G) . e in {x} by A150, A153, GLIB_000:def 18;
then (the_Source_of G) . e in (the_Vertices_of G) \ {x} by A152, XBOOLE_0:def 5;
then e DSJoins (the_Vertices_of G) \ {x},{x},G by A150, A153, GLIB_000:def 18;
hence e in G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} by GLIB_000:def 33; :: thesis:

end;

assume A154: e in G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:
then A155: e DSJoins (the_Vertices_of G) \ {x},{x},G by GLIB_000:def 33;
then A156: (the_Source_of G) . e in (the_Vertices_of G) \ {x} by GLIB_000:def 18;
then not (the_Source_of G) . e in {x} by XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 18;
then A157: not e in G .edgesDBetween {x},{x} by GLIB_000:def 33;
(the_Target_of G) . e in {x} by A155, GLIB_000:def 18;
then e DSJoins the_Vertices_of G,{x},G by A154, A156, GLIB_000:def 18;
then e in G .edgesDBetween (the_Vertices_of G),{x} by GLIB_000:def 33;
hence e in (G .edgesDBetween (the_Vertices_of G),{x}) \ (G .edgesDBetween {x},{x}) by A157, XBOOLE_0:def 5; :: thesis:

end;

then A158: (G .edgesDBetween (the_Vertices_of G),{x}) \ (G .edgesDBetween {x},{x}) = G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} by TARSKI:2;
A159: dom (EL | EXXfb) = EXXfb by PARTFUN1:def 4;

A160: now

let e be set ; :: thesis:
assume e in dom (EL | (G .edgesDBetween (the_Vertices_of G),{x})) ; :: thesis:
then A161: e in G .edgesDBetween (the_Vertices_of G),{x} by PARTFUN1:def 4;

now

per cases ;

suppose A162: e in G .edgesDBetween {x},{x} ; :: thesis:

then not e in EXXfb by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXfb)) . e = (EL | (G .edgesDBetween {x},{x})) . e by A159, FUNCT_4:12
.= EL . e by A162, FUNCT_1:72 ;
:: thesis:

end;

suppose not e in G .edgesDBetween {x},{x} ; :: thesis:

then A163: e in EXXfb by A161, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXfb)) . e = (EL | EXXfb) . e by A159, FUNCT_4:14
.= EL . e by A163, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | (G .edgesDBetween (the_Vertices_of G),{x})) . e = ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXfb)) . e by A161, FUNCT_1:72; :: thesis:

end;

now

let e be set ; :: thesis:

hereby :: thesis:

assume A164: e in (G .edgesDBetween {x},(the_Vertices_of G)) \ (G .edgesDBetween {x},{x}) ; :: thesis:
then e in G .edgesDBetween {x},(the_Vertices_of G) by XBOOLE_0:def 5;
then A165: e DSJoins {x}, the_Vertices_of G,G by GLIB_000:def 33;
then A166: (the_Target_of G) . e in the_Vertices_of G by GLIB_000:def 18;
A167: (the_Source_of G) . e in {x} by A165, GLIB_000:def 18;
not e in G .edgesDBetween {x},{x} by A164, XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 33;
then not (the_Target_of G) . e in {x} by A164, A167, GLIB_000:def 18;
then (the_Target_of G) . e in (the_Vertices_of G) \ {x} by A166, XBOOLE_0:def 5;
then e DSJoins {x},(the_Vertices_of G) \ {x},G by A164, A167, GLIB_000:def 18;
hence e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by GLIB_000:def 33; :: thesis:

end;

assume A168: e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) ; :: thesis:
then A169: e DSJoins {x},(the_Vertices_of G) \ {x},G by GLIB_000:def 33;
then A170: (the_Target_of G) . e in (the_Vertices_of G) \ {x} by GLIB_000:def 18;
then not (the_Target_of G) . e in {x} by XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 18;
then A171: not e in G .edgesDBetween {x},{x} by GLIB_000:def 33;
(the_Source_of G) . e in {x} by A169, GLIB_000:def 18;
then e DSJoins {x}, the_Vertices_of G,G by A168, A170, GLIB_000:def 18;
then e in G .edgesDBetween {x},(the_Vertices_of G) by GLIB_000:def 33;
hence e in (G .edgesDBetween {x},(the_Vertices_of G)) \ (G .edgesDBetween {x},{x}) by A171, XBOOLE_0:def 5; :: thesis:

end;

then A172: (G .edgesDBetween {x},(the_Vertices_of G)) \ (G .edgesDBetween {x},{x}) = G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by TARSKI:2;
A173: dom (EL | (G .edgesDBetween {x},(the_Vertices_of G))) = G .edgesDBetween {x},(the_Vertices_of G) by PARTFUN1:def 4;
A174: dom (EL | EXXeb) = EXXeb by PARTFUN1:def 4;

A175: now

let e be set ; :: thesis:
assume e in dom (EL | (G .edgesDBetween {x},(the_Vertices_of G))) ; :: thesis:
then A176: e in G .edgesDBetween {x},(the_Vertices_of G) by PARTFUN1:def 4;

now

per cases ;

suppose A177: e in G .edgesDBetween {x},{x} ; :: thesis:

then not e in EXXeb by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXeb)) . e = (EL | (G .edgesDBetween {x},{x})) . e by A174, FUNCT_4:12
.= EL . e by A177, FUNCT_1:72 ;
:: thesis:

end;

suppose not e in G .edgesDBetween {x},{x} ; :: thesis:

then A178: e in EXXeb by A176, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXeb)) . e = (EL | EXXeb) . e by A174, FUNCT_4:14
.= EL . e by A178, FUNCT_1:72 ;
:: thesis:

end;

hence (EL | (G .edgesDBetween {x},(the_Vertices_of G))) . e = ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXeb)) . e by A176, FUNCT_1:72; :: thesis:

end;

end;

hence S₁[n + 1] ; :: thesis:

end;

now

set ESS = G .edgesDBetween {sink},{sink};
let V be Subset of (the_Vertices_of G); :: thesis:
assume that
A182: card ((the_Vertices_of G) \ V) = 1 and
source in V and
A183: not sink in V ; :: thesis:
reconsider EOUT = (G .edgesOutOf {sink}) \ (G .edgesDBetween {sink},{sink}) as Subset of (the_Edges_of G) ;
consider v being set such that
A184: (the_Vertices_of G) \ V = {v} by A182, CARD_2:60;
sink is Vertex of G by A1, Def2;
then sink in (the_Vertices_of G) \ V by A183, XBOOLE_0:def 5;
then A185: v = sink by A184, TARSKI:def 1;

A186: now

let x be set ; :: thesis:

hereby :: thesis:

assume A187: x in (the_Vertices_of G) \ {sink} ; :: thesis:
then not x in {sink} by XBOOLE_0:def 5;
hence x in V by A184, A185, A187, XBOOLE_0:def 5; :: thesis:

end;

assume A188: x in V ; :: thesis:
then not x in {sink} by A183, TARSKI:def 1;
hence x in (the_Vertices_of G) \ {sink} by A188, XBOOLE_0:def 5; :: thesis:

end;

then A189: V = (the_Vertices_of G) \ {sink} by TARSKI:2;

now

let e be set ; :: thesis:

hereby :: thesis:

assume A190: e in G .edgesDBetween ((the_Vertices_of G) \ V),V ; :: thesis:
then A191: e DSJoins {sink},(the_Vertices_of G) \ {sink},G by A184, A185, A189, GLIB_000:def 33;
then A192: (the_Target_of G) . e in (the_Vertices_of G) \ {sink} by GLIB_000:def 18;

A193: now

assume e in G .edgesDBetween {sink},{sink} ; :: thesis:
then e DSJoins {sink},{sink},G by GLIB_000:def 33;
then (the_Target_of G) . e in {sink} by GLIB_000:def 18;
hence contradiction by A192, XBOOLE_0:def 5; :: thesis:

end;

(the_Source_of G) . e in {sink} by A191, GLIB_000:def 18;
then e in G .edgesOutOf {sink} by A190, GLIB_000:def 29;
hence e in EOUT by A193, XBOOLE_0:def 5; :: thesis:

end;

assume A194: e in EOUT ; :: thesis:
(G .edgesOutOf {sink}) \ (G .edgesDBetween {sink},{sink}) is Subset of (G .edgesOutOf {sink}) ;
then A195: (the_Source_of G) . e in {sink} by A194, GLIB_000:def 29;
A196: not e in G .edgesDBetween {sink},{sink} by A194, XBOOLE_0:def 5;

now

assume A197: not (the_Target_of G) . e in V ; :: thesis:
(the_Target_of G) . e in the_Vertices_of G by A194, FUNCT_2:7;
then (the_Target_of G) . e in {sink} by A189, A197, XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A194, A195, GLIB_000:def 18;
hence contradiction by A196, GLIB_000:def 33; :: thesis:

end;

then e DSJoins (the_Vertices_of G) \ V,V,G by A184, A185, A194, A195, GLIB_000:def 18;
hence e in G .edgesDBetween ((the_Vertices_of G) \ V),V by GLIB_000:def 33; :: thesis:

end;

then A198: G .edgesDBetween ((the_Vertices_of G) \ V),V = EOUT by TARSKI:2;
set EESS = EL | (G .edgesDBetween {sink},{sink});
reconsider EIN = (G .edgesInto {sink}) \ (G .edgesDBetween {sink},{sink}) as Subset of (the_Edges_of G) ;
A199: dom (EL | (G .edgesInto {sink})) = G .edgesInto {sink} by PARTFUN1:def 4;

now

let e be set ; :: thesis:

hereby :: thesis:

assume A200: e in G .edgesDBetween V,((the_Vertices_of G) \ V) ; :: thesis:
then A201: e DSJoins (the_Vertices_of G) \ {sink},{sink},G by A184, A185, A189, GLIB_000:def 33;
then A202: (the_Source_of G) . e in (the_Vertices_of G) \ {sink} by GLIB_000:def 18;

A203: now

assume e in G .edgesDBetween {sink},{sink} ; :: thesis:
then e DSJoins {sink},{sink},G by GLIB_000:def 33;
then (the_Source_of G) . e in {sink} by GLIB_000:def 18;
hence contradiction by A202, XBOOLE_0:def 5; :: thesis:

end;

(the_Target_of G) . e in {sink} by A201, GLIB_000:def 18;
then e in G .edgesInto {sink} by A200, GLIB_000:def 28;
hence e in EIN by A203, XBOOLE_0:def 5; :: thesis:

end;

assume A204: e in EIN ; :: thesis:
(G .edgesInto {sink}) \ (G .edgesDBetween {sink},{sink}) is Subset of (G .edgesInto {sink}) ;
then A205: (the_Target_of G) . e in {sink} by A204, GLIB_000:def 28;
A206: not e in G .edgesDBetween {sink},{sink} by A204, XBOOLE_0:def 5;

now

assume not (the_Source_of G) . e in V ; :: thesis:
then A207: not (the_Source_of G) . e in (the_Vertices_of G) \ {sink} by A186;
(the_Source_of G) . e in the_Vertices_of G by A204, FUNCT_2:7;
then (the_Source_of G) . e in {sink} by A207, XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A204, A205, GLIB_000:def 18;
hence contradiction by A206, GLIB_000:def 33; :: thesis:

end;

then e DSJoins V,{sink},G by A204, A205, GLIB_000:def 18;
hence e in G .edgesDBetween V,((the_Vertices_of G) \ V) by A184, A185, GLIB_000:def 33; :: thesis:

end;

then A208: G .edgesDBetween V,((the_Vertices_of G) \ V) = EIN by TARSKI:2;

now

let e be set ; :: thesis:
assume A209: e in G .edgesDBetween {sink},{sink} ; :: thesis:
then e DSJoins {sink},{sink},G by GLIB_000:def 33;
then (the_Source_of G) . e in {sink} by GLIB_000:def 18;
hence e in G .edgesOutOf {sink} by A209, GLIB_000:def 29; :: thesis:

end;

then A210: G .edgesDBetween {sink},{sink} c= G .edgesOutOf {sink} by TARSKI:def 3;

now

let e be set ; :: thesis:
assume A211: e in G .edgesDBetween {sink},{sink} ; :: thesis:
then e DSJoins {sink},{sink},G by GLIB_000:def 33;
then (the_Target_of G) . e in {sink} by GLIB_000:def 18;
hence e in G .edgesInto {sink} by A211, GLIB_000:def 28; :: thesis:

end;

then A212: G .edgesDBetween {sink},{sink} c= G .edgesInto {sink} by TARSKI:def 3;
A213: dom (EL | (G .edgesDBetween {sink},{sink})) = G .edgesDBetween {sink},{sink} by PARTFUN1:def 4;
A214: dom (EL | EOUT) = EOUT by PARTFUN1:def 4;

A215: now

let e be set ; :: thesis:
assume A216: e in dom (EL | (G .edgesOutOf {sink})) ; :: thesis:
then A217: e in G .edgesOutOf {sink} by PARTFUN1:def 4;

now

per cases ;

suppose A218: e in G .edgesDBetween {sink},{sink} ; :: thesis:

then not e in EOUT by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EOUT)) . e = (EL | (G .edgesDBetween {sink},{sink})) . e by A214, FUNCT_4:12
.= EL . e by A213, A218, FUNCT_1:70 ;
:: thesis:

end;

suppose not e in G .edgesDBetween {sink},{sink} ; :: thesis:

then A219: e in EOUT by A217, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EOUT)) . e = (EL | EOUT) . e by A214, FUNCT_4:14
.= EL . e by A214, A219, FUNCT_1:70 ;
:: thesis:

end;

hence (EL | (G .edgesOutOf {sink})) . e = ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EOUT)) . e by A216, FUNCT_1:70; :: thesis:

end;

A220: dom (EL | EIN) = EIN by PARTFUN1:def 4;

A221: now

let e be set ; :: thesis:
assume A222: e in dom (EL | (G .edgesInto {sink})) ; :: thesis:
then A223: e in G .edgesInto {sink} by PARTFUN1:def 4;

now

per cases ;

suppose A224: e in G .edgesDBetween {sink},{sink} ; :: thesis:

then not e in EIN by XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EIN)) . e = (EL | (G .edgesDBetween {sink},{sink})) . e by A220, FUNCT_4:12
.= EL . e by A213, A224, FUNCT_1:70 ;
:: thesis:

end;

suppose not e in G .edgesDBetween {sink},{sink} ; :: thesis:

then A225: e in EIN by A223, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EIN)) . e = (EL | EIN) . e by A220, FUNCT_4:14
.= EL . e by A220, A225, FUNCT_1:70 ;
:: thesis:

end;

hence (EL | (G .edgesInto {sink})) . e = ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EIN)) . e by A222, FUNCT_1:70; :: thesis:

end;

end;

then A229: S₁[1] ;
for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A229, A6);
hence EL .flow source,sink = (Sum (EL | (G .edgesDBetween V,((the_Vertices_of G) \ V)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V),V))) by A2, A3, A4; :: thesis: