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

assume card ((the_Vertices_of G) \ V) = 0 ; :: thesis:
then A5: (the_Vertices_of G) \ V = {} ;
sink is Vertex of G by A1;
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 :: thesis:

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

now :: thesis:

now :: thesis:

end;

now :: thesis:

end;

then A25: G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) c= G .edgesDBetween ((V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) ;

now :: thesis:

end;

then (G .edgesDBetween ((V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})))) \ (G .edgesDBetween (V2,{ the Element of ((the_Vertices_of G) \ V2) \ {sink}})) = G .edgesDBetween ((V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) by XBOOLE_1:83;
then A28: EB = G .edgesDBetween ((V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) by XBOOLE_1:40;
A29: dom (EL | EB) = EB by PARTFUN1:def 2;

A30: now :: thesis:

let e be object ; :: thesis:
assume e in dom (EL | EA) ; :: thesis:
then A31: e in EA ;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

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

end;

now :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

end;

end;

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

A47: now :: thesis:

let e be object ; :: thesis:
assume e in dom (EL | EC) ; :: thesis:
then A48: e in EC ;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

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

end;

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

now :: thesis:

let e be object ; :: thesis:

hereby :: thesis:

end;

end;

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

now :: thesis:

end;

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

now :: thesis:

end;

then A73: G .edgesDBetween (V2,{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) c= G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) ;
A74: V2 \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}} is Subset of V2 ;

now :: thesis:

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 31;
then A78: (the_Source_of G) . e in V2 ;

A79: now :: thesis:

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

end;

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

now :: thesis:

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

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

end;

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

end;

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

end;

now :: thesis:

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

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

then A85: e DSJoins V1,(the_Vertices_of G) \ V1,G by GLIB_000:def 31;
then A86: (the_Source_of G) . e in V1 ;
A87: (the_Target_of G) . e in (the_Vertices_of G) \ V1 by A85;
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 { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by A83, A84, A87;
then (the_Source_of G) . e in V1 \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by A86, XBOOLE_0:def 5;
then (the_Source_of G) . e in V2 \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by XBOOLE_1:40;
hence e DSJoins V2,(the_Vertices_of G) \ V2,G by A74, A84, A88; :: thesis:

end;

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

then A90: e DSJoins V2,{ the Element of ((the_Vertices_of G) \ V2) \ {sink}},G by GLIB_000:def 31;
then A91: (the_Source_of G) . e in V2 ;
(the_Target_of G) . e in { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by A90;
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:5;
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; :: thesis:

end;

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

end;

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

now :: thesis:

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 31;
then A97: (the_Target_of G) . e in V2 ;

A98: now :: thesis:

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

end;

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

now :: thesis:

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

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

end;

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

end;

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

end;

now :: thesis:

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

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

then A104: e DSJoins (the_Vertices_of G) \ V1,V1,G by GLIB_000:def 31;
then A105: (the_Target_of G) . e in V1 ;
A106: (the_Source_of G) . e in (the_Vertices_of G) \ V1 by A104;
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 { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by A102, A103, A106;
then (the_Target_of G) . e in V1 \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by A105, XBOOLE_0:def 5;
then (the_Target_of G) . e in V2 \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by XBOOLE_1:40;
hence e DSJoins (the_Vertices_of G) \ V2,V2,G by A74, A103, A107; :: thesis:

end;

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

then A109: e DSJoins { the Element of ((the_Vertices_of G) \ V2) \ {sink}},V2,G by GLIB_000:def 31;
then A110: (the_Target_of G) . e in V2 ;
(the_Source_of G) . e in { the Element of ((the_Vertices_of G) \ V2) \ {sink}} by A109;
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:5;
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; :: thesis:

end;

hence e in G .edgesDBetween (((the_Vertices_of G) \ V2),V2) by GLIB_000:def 31; :: 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 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}})) by PARTFUN1:def 2;

A114: now :: thesis:

let e be object ; :: thesis:
assume e in dom (EL | EC) ; :: thesis:
then A115: e in EC ;

now :: thesis:

per cases ;

suppose not e in G .edgesDBetween (((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})),{ the Element of ((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 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) +* (EL | E2)) . e = (EL | E2) . e by A113, FUNCT_4:13
.= EL . e by A116, FUNCT_1:49 ;
:: thesis:

end;

suppose A117: e in G .edgesDBetween (((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})),{ the Element of ((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 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) +* (EL | E2)) . e = (EL | (G .edgesDBetween (((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) . e by A113, FUNCT_4:11
.= EL . e by A117, FUNCT_1:49 ;
:: thesis:

end;

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

end;

now :: thesis:

end;

then A126: G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},V2) c= G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})) ;
A127: dom (EL | E1) = EA \ (G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ (V2 \/ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})))) by PARTFUN1:def 2;

A128: now :: thesis:

let e be object ; :: thesis:
assume e in dom (EL | EA) ; :: thesis:
then A129: e in EA ;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

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

end;

A132: dom (EL | (G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) = G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) by PARTFUN1:def 2;

A133: now :: thesis:

let e be object ; :: thesis:
assume A134: e in dom (EL | (G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) ; :: thesis:
then A135: e in G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) ;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

hence (EL | (G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) . e = ((EL | (G .edgesDBetween (V2,{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}))) +* (EL | EV1Xdb)) . e by A134, FUNCT_1:49; :: thesis:

end;

A142: now :: thesis:

let e be object ; :: thesis:
assume A143: e in dom (EL | (G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})))) ; :: thesis:
then A144: e in G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})) ;

now :: thesis:

per cases ;

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

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

end;

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

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

end;

hence (EL | (G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})))) . e = ((EL | (G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},V2))) +* (EL | EXV1cb)) . e by A143, FUNCT_1:49; :: thesis:

end;

now :: thesis:

let e be object ; :: 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 31;
then A152: (the_Source_of G) . e in the_Vertices_of G ;
A153: (the_Target_of G) . e in {x} by A151;
not e in G .edgesDBetween ({x},{x}) by A150, XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 31;
then not (the_Source_of G) . e in {x} by A150, A153;
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;
hence e in G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) by GLIB_000:def 31; :: thesis:

end;

assume A154: e in G .edgesDBetween (((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) ; :: thesis:
then A155: e DSJoins (the_Vertices_of G) \ {x},{x},G by GLIB_000:def 31;
then A156: (the_Source_of G) . e in (the_Vertices_of G) \ {x} ;
then not (the_Source_of G) . e in {x} by XBOOLE_0:def 5;
then not e DSJoins {x},{x},G ;
then A157: not e in G .edgesDBetween ({x},{x}) by GLIB_000:def 31;
(the_Target_of G) . e in {x} by A155;
then e DSJoins the_Vertices_of G,{x},G by A154, A156;
then e in G .edgesDBetween ((the_Vertices_of G),{x}) by GLIB_000:def 31;
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) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}}),{ the Element of ((the_Vertices_of G) \ V2) \ {sink}}) by TARSKI:2;
A159: dom (EL | EXXfb) = EXXfb by PARTFUN1:def 2;

A160: now :: thesis:

let e be object ; :: 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}) ;

now :: thesis:

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:11
.= EL . e by A162, FUNCT_1:49 ;
:: 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:13
.= EL . e by A163, FUNCT_1:49 ;
:: thesis:

end;

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

end;

now :: thesis:

let e be object ; :: 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 31;
then A166: (the_Target_of G) . e in the_Vertices_of G ;
A167: (the_Source_of G) . e in {x} by A165;
not e in G .edgesDBetween ({x},{x}) by A164, XBOOLE_0:def 5;
then not e DSJoins {x},{x},G by GLIB_000:def 31;
then not (the_Target_of G) . e in {x} by A164, A167;
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;
hence e in G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})) by GLIB_000:def 31; :: thesis:

end;

assume A168: e in G .edgesDBetween ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((the_Vertices_of G) \ V2) \ {sink}})) ; :: thesis:
then A169: e DSJoins {x},(the_Vertices_of G) \ {x},G by GLIB_000:def 31;
then A170: (the_Target_of G) . e in (the_Vertices_of G) \ {x} ;
then not (the_Target_of G) . e in {x} by XBOOLE_0:def 5;
then not e DSJoins {x},{x},G ;
then A171: not e in G .edgesDBetween ({x},{x}) by GLIB_000:def 31;
(the_Source_of G) . e in {x} by A169;
then e DSJoins {x}, the_Vertices_of G,G by A168, A170;
then e in G .edgesDBetween ({x},(the_Vertices_of G)) by GLIB_000:def 31;
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 ({ the Element of ((the_Vertices_of G) \ V2) \ {sink}},((the_Vertices_of G) \ { the Element of ((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 2;
A174: dom (EL | EXXeb) = EXXeb by PARTFUN1:def 2;

A175: now :: thesis:

let e be object ; :: 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)) ;

now :: thesis:

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:11
.= EL . e by A177, FUNCT_1:49 ;
:: 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:13
.= EL . e by A178, FUNCT_1:49 ;
:: thesis:

end;

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

end;

end;

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

end;

now :: thesis:

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 object such that
A184: (the_Vertices_of G) \ V = {v} by A182, CARD_2:42;
sink is Vertex of G by A1;
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 :: thesis:

let x be object ; :: 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 :: thesis:

let e be object ; :: 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 31;
then A192: (the_Target_of G) . e in (the_Vertices_of G) \ {sink} ;

A193: now :: thesis:

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

end;

(the_Source_of G) . e in {sink} by A191;
then e in G .edgesOutOf {sink} by A190, GLIB_000:def 27;
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 27;
A196: not e in G .edgesDBetween ({sink},{sink}) by A194, XBOOLE_0:def 5;

now :: thesis:

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:5;
then (the_Target_of G) . e in {sink} by A189, A197, XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A194, A195;
hence contradiction by A196, GLIB_000:def 31; :: thesis:

end;

then e DSJoins (the_Vertices_of G) \ V,V,G by A184, A185, A194, A195;
hence e in G .edgesDBetween (((the_Vertices_of G) \ V),V) by GLIB_000:def 31; :: 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 2;

now :: thesis:

let e be object ; :: 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 31;
then A202: (the_Source_of G) . e in (the_Vertices_of G) \ {sink} ;

A203: now :: thesis:

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

end;

(the_Target_of G) . e in {sink} by A201;
then e in G .edgesInto {sink} by A200, GLIB_000:def 26;
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 26;
A206: not e in G .edgesDBetween ({sink},{sink}) by A204, XBOOLE_0:def 5;

now :: thesis:

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:5;
then (the_Source_of G) . e in {sink} by A207, XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A204, A205;
hence contradiction by A206, GLIB_000:def 31; :: thesis:

end;

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

end;

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

now :: thesis:

let e be object ; :: thesis:
assume A209: e in G .edgesDBetween ({sink},{sink}) ; :: thesis:
then e DSJoins {sink},{sink},G by GLIB_000:def 31;
then (the_Source_of G) . e in {sink} ;
hence e in G .edgesOutOf {sink} by A209, GLIB_000:def 27; :: thesis:

end;

then A210: G .edgesDBetween ({sink},{sink}) c= G .edgesOutOf {sink} ;

now :: thesis:

let e be object ; :: thesis:
assume A211: e in G .edgesDBetween ({sink},{sink}) ; :: thesis:
then e DSJoins {sink},{sink},G by GLIB_000:def 31;
then (the_Target_of G) . e in {sink} ;
hence e in G .edgesInto {sink} by A211, GLIB_000:def 26; :: thesis:

end;

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

A215: now :: thesis:

let e be object ; :: thesis:
assume A216: e in dom (EL | (G .edgesOutOf {sink})) ; :: thesis:
then A217: e in G .edgesOutOf {sink} ;

now :: thesis:

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:11
.= EL . e by A213, A218, FUNCT_1:47 ;
:: 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:13
.= EL . e by A214, A219, FUNCT_1:47 ;
:: thesis:

end;

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

end;

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

A221: now :: thesis:

let e be object ; :: thesis:
assume A222: e in dom (EL | (G .edgesInto {sink})) ; :: thesis:
then A223: e in G .edgesInto {sink} ;

now :: thesis:

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:11
.= EL . e by A213, A224, FUNCT_1:47 ;
:: 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:13
.= EL . e by A220, A225, FUNCT_1:47 ;
:: thesis:

end;

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

end;

A226: (G .edgesDBetween ({sink},{sink})) \/ EIN = (G .edgesInto {sink}) \/ (G .edgesDBetween ({sink},{sink})) by XBOOLE_1:39
.= G .edgesInto {sink} by A212, XBOOLE_1:12 ;
dom ((EL | (G .edgesDBetween ({sink},{sink}))) +* (EL | EIN)) = (G .edgesDBetween ({sink},{sink})) \/ EIN by A213, A220, FUNCT_4:def 1;
then A227: Sum (EL | (G .edgesInto {sink})) = (Sum (EL | EIN)) + (Sum (EL | (G .edgesDBetween ({sink},{sink})))) by A226, A199, A221, FUNCT_1:2, GLIB_004:3;
(G .edgesDBetween ({sink},{sink})) \/ EOUT = (G .edgesOutOf {sink}) \/ (G .edgesDBetween ({sink},{sink})) by XBOOLE_1:39
.= G .edgesOutOf {sink} by A210, XBOOLE_1:12 ;
then A228: dom ((EL | (G .edgesDBetween ({sink},{sink}))) +* (EL | EOUT)) = G .edgesOutOf {sink} by A213, A214, FUNCT_4:def 1;
dom (EL | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} by PARTFUN1:def 2;
then EL .flow (source,sink) = ((Sum (EL | EIN)) + (Sum (EL | (G .edgesDBetween ({sink},{sink}))))) - ((Sum (EL | (G .edgesDBetween ({sink},{sink})))) + (Sum (EL | EOUT))) by A227, A228, A215, FUNCT_1:2, GLIB_004:3
.= (Sum (EL | EIN)) - (Sum (EL | EOUT)) ;
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 A208, A198; :: thesis:

end;

then A229: S₁[1] ;
for n being non zero 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: