let G be finite real-weighted WGraph; :: thesis:
let EL be FF:ELabeling of ; :: thesis:
let source, sink be set ; :: thesis:
let V be Subset of (the_Vertices_of G); :: thesis:
assume A1: ( EL has_valid_flow_from source,sink & source in V & not sink in V ) ; :: thesis:
set VG = the_Vertices_of G;
set SG = the_Source_of G;
set TG = the_Target_of G;
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)));

now

let V be Subset of (the_Vertices_of G); :: thesis:
assume A2: ( card ((the_Vertices_of G) \ V) = 1 & source in V & not sink in V ) ; :: thesis:
then consider v being set such that
A3: (the_Vertices_of G) \ V = {v} by CARD_2:60;
sink is Vertex of G by A1, Def7;
then sink in (the_Vertices_of G) \ V by A2, XBOOLE_0:def 5;
then A4: v = sink by A3, TARSKI:def 1;

A5: now

let x be set ; :: thesis:

hereby :: thesis:

assume x in (the_Vertices_of G) \ {sink} ; :: thesis:
then ( x in the_Vertices_of G & not x in {sink} ) by XBOOLE_0:def 5;
hence x in V by A3, A4, XBOOLE_0:def 5; :: thesis:

end;

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

end;

then A7: V = (the_Vertices_of G) \ {sink} by TARSKI:2;
set ESS = G .edgesDBetween {sink},{sink};
reconsider EIN = (G .edgesInto {sink}) \ (G .edgesDBetween {sink},{sink}) as Subset of (the_Edges_of G) ;
reconsider EOUT = (G .edgesOutOf {sink}) \ (G .edgesDBetween {sink},{sink}) as Subset of (the_Edges_of G) ;
set EESS = EL | (G .edgesDBetween {sink},{sink});

now

let e be set ; :: thesis:

hereby :: thesis:

assume e in G .edgesDBetween V,((the_Vertices_of G) \ V) ; :: thesis:
then e DSJoins (the_Vertices_of G) \ {sink},{sink},G by A3, A4, A7, GLIB_000:def 33;
then A8: ( e in the_Edges_of G & (the_Source_of G) . e in (the_Vertices_of G) \ {sink} & (the_Target_of G) . e in {sink} ) by GLIB_000:def 18;
then A9: e in G .edgesInto {sink} by GLIB_000:def 28;

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 A8, XBOOLE_0:def 5; :: thesis:

end;

hence e in EIN by A9, XBOOLE_0:def 5; :: thesis:

end;

assume A10: e in EIN ; :: thesis:
then A11: ( e in G .edgesInto {sink} & not e in G .edgesDBetween {sink},{sink} ) by XBOOLE_0:def 5;
(G .edgesInto {sink}) \ (G .edgesDBetween {sink},{sink}) is Subset of (G .edgesInto {sink}) ;
then A12: ( e in the_Edges_of G & (the_Target_of G) . e in {sink} ) by A10, GLIB_000:def 28;

now

assume not (the_Source_of G) . e in V ; :: thesis:
then A13: not (the_Source_of G) . e in (the_Vertices_of G) \ {sink} by A5;
(the_Source_of G) . e in the_Vertices_of G by A10, FUNCT_2:7;
then (the_Source_of G) . e in {sink} by A13, XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A12, GLIB_000:def 18;
hence contradiction by A11, GLIB_000:def 33; :: thesis:

end;

then e DSJoins V,{sink},G by A12, GLIB_000:def 18;
hence e in G .edgesDBetween V,((the_Vertices_of G) \ V) by A3, A4, GLIB_000:def 33; :: thesis:

end;

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

now

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

end;

then A15: G .edgesDBetween {sink},{sink} c= G .edgesInto {sink} by TARSKI:def 3;
A16: (G .edgesDBetween {sink},{sink}) \/ EIN = (G .edgesInto {sink}) \/ (G .edgesDBetween {sink},{sink}) by XBOOLE_1:39
.= G .edgesInto {sink} by A15, XBOOLE_1:12 ;
A17: ( dom (EL | (G .edgesInto {sink})) = G .edgesInto {sink} & dom (EL | (G .edgesDBetween {sink},{sink})) = G .edgesDBetween {sink},{sink} & dom (EL | EIN) = EIN & dom (EL | EOUT) = EOUT & dom (EL | (G .edgesOutOf {sink})) = G .edgesOutOf {sink} ) by PARTFUN1:def 4;
then A18: dom ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EIN)) = (G .edgesDBetween {sink},{sink}) \/ EIN by FUNCT_4:def 1;

now

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

now

per cases ;

suppose A21: 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 A17, FUNCT_4:12
.= EL . e by A17, A21, FUNCT_1:70 ;
:: thesis:

end;

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

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

end;

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

end;

then A23: Sum (EL | (G .edgesInto {sink})) = (Sum (EL | EIN)) + (Sum (EL | (G .edgesDBetween {sink},{sink}))) by A16, A17, A18, FUNCT_1:9, GLIB_004:3;

now

let e be set ; :: thesis:

hereby :: thesis:

assume e in G .edgesDBetween ((the_Vertices_of G) \ V),V ; :: thesis:
then e DSJoins {sink},(the_Vertices_of G) \ {sink},G by A3, A4, A7, GLIB_000:def 33;
then A24: ( e in the_Edges_of G & (the_Source_of G) . e in {sink} & (the_Target_of G) . e in (the_Vertices_of G) \ {sink} ) by GLIB_000:def 18;
then A25: e in G .edgesOutOf {sink} by GLIB_000:def 29;

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 A24, XBOOLE_0:def 5; :: thesis:

end;

hence e in EOUT by A25, XBOOLE_0:def 5; :: thesis:

end;

assume A26: e in EOUT ; :: thesis:
then A27: ( e in G .edgesOutOf {sink} & not e in G .edgesDBetween {sink},{sink} ) by XBOOLE_0:def 5;
(G .edgesOutOf {sink}) \ (G .edgesDBetween {sink},{sink}) is Subset of (G .edgesOutOf {sink}) ;
then A28: ( e in the_Edges_of G & (the_Source_of G) . e in {sink} ) by A26, GLIB_000:def 29;

now

assume A29: not (the_Target_of G) . e in V ; :: thesis:
(the_Target_of G) . e in the_Vertices_of G by A26, FUNCT_2:7;
then (the_Target_of G) . e in {sink} by A7, A29, XBOOLE_0:def 5;
then e DSJoins {sink},{sink},G by A28, GLIB_000:def 18;
hence contradiction by A27, GLIB_000:def 33; :: thesis:

end;

then e DSJoins (the_Vertices_of G) \ V,V,G by A3, A4, A28, GLIB_000:def 18;
hence e in G .edgesDBetween ((the_Vertices_of G) \ V),V by GLIB_000:def 33; :: thesis:

end;

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

now

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

end;

then A31: G .edgesDBetween {sink},{sink} c= G .edgesOutOf {sink} by TARSKI:def 3;
(G .edgesDBetween {sink},{sink}) \/ EOUT = (G .edgesOutOf {sink}) \/ (G .edgesDBetween {sink},{sink}) by XBOOLE_1:39
.= G .edgesOutOf {sink} by A31, XBOOLE_1:12 ;
then A32: dom ((EL | (G .edgesDBetween {sink},{sink})) +* (EL | EOUT)) = G .edgesOutOf {sink} by A17, FUNCT_4:def 1;

now

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

now

per cases ;

suppose A35: 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 A17, FUNCT_4:12
.= EL . e by A17, A35, FUNCT_1:70 ;
:: thesis:

end;

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

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

end;

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

end;

then Sum (EL | (G .edgesOutOf {sink})) = (Sum (EL | EOUT)) + (Sum (EL | (G .edgesDBetween {sink},{sink}))) by A17, A32, FUNCT_1:9, GLIB_004:3;
then EL .flow source,sink = ((Sum (EL | EIN)) + (Sum (EL | (G .edgesDBetween {sink},{sink})))) - ((Sum (EL | (G .edgesDBetween {sink},{sink}))) + (Sum (EL | EOUT))) by A1, A23, Def8
.= (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 A14, A30; :: thesis:

end;

then A37: S₁[1] ;

A38: now

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

now

let V2 be Subset of (the_Vertices_of G); :: thesis:
assume A40: ( card ((the_Vertices_of G) \ V2) = n + 1 & source in V2 & not sink in V2 ) ; :: thesis:
set x = choose (((the_Vertices_of G) \ V2) \ {sink});
A41: V2 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} is Subset of V2 ;
sink is Vertex of G by A1, Def7;
then sink in (the_Vertices_of G) \ V2 by A40, XBOOLE_0:def 5;
then {sink} c= (the_Vertices_of G) \ V2 by ZFMISC_1:37;
then card (((the_Vertices_of G) \ V2) \ {sink}) = (n + 1) - (card {sink}) by A40, CARD_2:63
.= (n + 1) - 1 by CARD_1:50
.= n ;
then A42: ( choose (((the_Vertices_of G) \ V2) \ {sink}) in (the_Vertices_of G) \ V2 & not choose (((the_Vertices_of G) \ V2) \ {sink}) in {sink} ) by CARD_1:47, XBOOLE_0:def 5;
then A43: ( choose (((the_Vertices_of G) \ V2) \ {sink}) in the_Vertices_of G & not choose (((the_Vertices_of G) \ V2) \ {sink}) in V2 ) by XBOOLE_0:def 5;
set V1 = V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))};
set EV1V1a = G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}));
set EV1V1b = G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),(V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))});
set EV2X = G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))};
set EXV2 = G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2;
set EXV1c = G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}));
set EV1Xd = G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))};
{(choose (((the_Vertices_of G) \ V2) \ {sink}))} c= the_Vertices_of G by A42, ZFMISC_1:37;
then reconsider V1 = V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} as Subset of (the_Vertices_of G) by XBOOLE_1:8;
A44: (the_Vertices_of G) \ V1 = ((the_Vertices_of G) \ V2) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by XBOOLE_1:41;
{(choose (((the_Vertices_of G) \ V2) \ {sink}))} c= (the_Vertices_of G) \ V2 by A42, ZFMISC_1:37;
then A45: card ((the_Vertices_of G) \ V1) = (card ((the_Vertices_of G) \ V2)) - (card {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) by A44, CARD_2:63
.= (n + 1) - 1 by A40, CARD_1:50
.= n ;
A46: source in V1 by A40, XBOOLE_0:def 3;
A47: choose (((the_Vertices_of G) \ V2) \ {sink}) <> sink by A42, TARSKI:def 1;
then not sink in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by TARSKI:def 1;
then not sink in V1 by A40, XBOOLE_0:def 3;
then A48: EL .flow source,sink = (Sum (EL | (G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),(V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) by A39, A45, A46;

now

let e be set ; :: thesis:

hereby :: thesis:

assume e in G .edgesDBetween V2,((the_Vertices_of G) \ V2) ; :: thesis:
then e DSJoins V2,(the_Vertices_of G) \ V2,G by GLIB_000:def 33;
then A49: ( e in the_Edges_of G & (the_Source_of G) . e in V2 & (the_Target_of G) . e in (the_Vertices_of G) \ V2 ) by GLIB_000:def 18;
then A50: (the_Source_of G) . e in V1 by XBOOLE_0:def 3;

A51: now

end;

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 A52, A54, XBOOLE_0:def 3;

suppose 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 e DSJoins V1,(the_Vertices_of G) \ V1,G by GLIB_000:def 33;
then A55: ( e in the_Edges_of G & (the_Source_of G) . e in V1 & (the_Target_of G) . e in (the_Vertices_of G) \ V1 ) by GLIB_000:def 18;
then not (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A53, GLIB_000:def 18;
then (the_Source_of G) . e in V1 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A55, XBOOLE_0:def 5;
then A56: (the_Source_of G) . e in V2 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by XBOOLE_1:40;
( (the_Target_of G) . e in the_Vertices_of G & not (the_Target_of G) . e in V1 ) by A55, XBOOLE_0:def 5;
then not (the_Target_of G) . e in V2 by XBOOLE_0:def 3;
then (the_Target_of G) . e in (the_Vertices_of G) \ V2 by A55, XBOOLE_0:def 5;
hence e DSJoins V2,(the_Vertices_of G) \ V2,G by A41, A55, A56, GLIB_000:def 18; :: thesis:

end;

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

then e DSJoins V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))},G by GLIB_000:def 33;
then A57: ( e in the_Edges_of G & (the_Source_of G) . e in V2 & (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ) by GLIB_000:def 18;
then A58: (the_Target_of G) . e in the_Vertices_of G by FUNCT_2:7;
not (the_Target_of G) . e in V2 by A43, A57, TARSKI:def 1;
then (the_Target_of G) . e in (the_Vertices_of G) \ V2 by A58, XBOOLE_0:def 5;
hence e DSJoins V2,(the_Vertices_of G) \ V2,G by A57, GLIB_000:def 18; :: thesis:

end;

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

end;

now

end;

now

end;

now

end;

now

let e be set ; :: thesis:
assume e in dom (EL | EA) ; :: thesis:
then A68: 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 A69: e in E1 by A68, 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 A66, FUNCT_4:14
.= EL . e by A69, FUNCT_1:72 ;
:: thesis:

end;

suppose A70: 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 A66, FUNCT_4:12
.= EL . e by A70, 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 A68, FUNCT_1:72; :: thesis:

end;

then A71: Sum (EL | EA) = (Sum (EL | E1)) + (Sum (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))))) by A66, A67, FUNCT_1:9, GLIB_004:3;
A72: dom ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EB)) = (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))}) \/ EB by A66, FUNCT_4:def 1
.= (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))}) \/ ((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}))})) by XBOOLE_1:39
.= EA by XBOOLE_1:6 ;

now

let e be set ; :: thesis:
assume e in dom (EL | EA) ; :: thesis:
then A73: 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 A74: e in EB by A73, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EB)) . e = (EL | EB) . e by A66, FUNCT_4:14
.= EL . e by A74, FUNCT_1:72 ;
:: thesis:

end;

suppose A75: 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 A66, FUNCT_4:12
.= EL . e by A75, FUNCT_1:72 ;
:: thesis:

end;

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

end;

then A76: Sum (EL | EA) = (Sum (EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) + (Sum (EL | (G .edgesDBetween (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))))) by A61, A66, A72, FUNCT_1:9, GLIB_004:3;

now

end;

then A78: 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;

now

let e be set ; :: thesis:

hereby :: thesis:

assume e in G .edgesDBetween ((the_Vertices_of G) \ V2),V2 ; :: thesis:
then e DSJoins (the_Vertices_of G) \ V2,V2,G by GLIB_000:def 33;
then A79: ( e in the_Edges_of G & (the_Target_of G) . e in V2 & (the_Source_of G) . e in (the_Vertices_of G) \ V2 ) by GLIB_000:def 18;
then A80: (the_Target_of G) . e in V1 by XBOOLE_0:def 3;

A81: now

end;

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 A82, A84, XBOOLE_0:def 3;

suppose 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 e DSJoins (the_Vertices_of G) \ V1,V1,G by GLIB_000:def 33;
then A85: ( e in the_Edges_of G & (the_Target_of G) . e in V1 & (the_Source_of G) . e in (the_Vertices_of G) \ V1 ) by GLIB_000:def 18;
then not (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A83, GLIB_000:def 18;
then (the_Target_of G) . e in V1 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A85, XBOOLE_0:def 5;
then A86: (the_Target_of G) . e in V2 \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by XBOOLE_1:40;
( (the_Source_of G) . e in the_Vertices_of G & not (the_Source_of G) . e in V1 ) by A85, XBOOLE_0:def 5;
then not (the_Source_of G) . e in V2 by XBOOLE_0:def 3;
then (the_Source_of G) . e in (the_Vertices_of G) \ V2 by A85, XBOOLE_0:def 5;
hence e DSJoins (the_Vertices_of G) \ V2,V2,G by A41, A85, A86, GLIB_000:def 18; :: thesis:

end;

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

then e DSJoins {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2,G by GLIB_000:def 33;
then A87: ( e in the_Edges_of G & (the_Target_of G) . e in V2 & (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ) by GLIB_000:def 18;
then A88: (the_Source_of G) . e in the_Vertices_of G by FUNCT_2:7;
not (the_Source_of G) . e in V2 by A43, A87, TARSKI:def 1;
then (the_Source_of G) . e in (the_Vertices_of G) \ V2 by A88, XBOOLE_0:def 5;
hence e DSJoins (the_Vertices_of G) \ V2,V2,G by A87, GLIB_000:def 18; :: thesis:

end;

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

end;

now

let e be set ; :: thesis:
assume e in dom (EL | EC) ; :: thesis:
then A92: 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 A93: e in E2 by A92, 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 A90, FUNCT_4:14
.= EL . e by A93, FUNCT_1:72 ;
:: thesis:

end;

suppose A94: 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 A90, FUNCT_4:12
.= EL . e by A94, 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 A92, FUNCT_1:72; :: thesis:

end;

then A95: Sum (EL | EC) = (Sum (EL | E2)) + (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) by A90, A91, FUNCT_1:9, GLIB_004:3;
A96: dom ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | ED)) = (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2) \/ ED by A90, FUNCT_4:def 1
.= (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2) \/ ((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)) by XBOOLE_1:39
.= EC by XBOOLE_1:6 ;

now

let e be set ; :: thesis:
assume e in dom (EL | EC) ; :: thesis:
then A97: 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 A98: e in ED by A97, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | ED)) . e = (EL | ED) . e by A90, FUNCT_4:14
.= EL . e by A98, FUNCT_1:72 ;
:: thesis:

end;

suppose A99: 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 A90, FUNCT_4:12
.= EL . e by A99, FUNCT_1:72 ;
:: thesis:

end;

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

end;

then A100: Sum (EL | EC) = (Sum (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2))) + (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),(V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) by A63, A90, A96, FUNCT_1:9, GLIB_004:3;
set EXXe = G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))});
set EXXf = G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))};

now

let e be set ; :: thesis:

hereby :: thesis:

end;

end;

now

let e be set ; :: thesis:
assume e in G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:
then e DSJoins V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))},G by GLIB_000:def 33;
then A108: ( e in the_Edges_of G & (the_Source_of G) . e in V2 & (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ) by GLIB_000:def 18;
then not (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A43, TARSKI:def 1;
then (the_Source_of G) . e in (the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A108, XBOOLE_0:def 5;
then e DSJoins (the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))},{(choose (((the_Vertices_of G) \ V2) \ {sink}))},G by A108, 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;

now

let e be set ; :: thesis:
assume A112: 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 A113: 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 A114: 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 A110, FUNCT_4:12
.= EL . e by A114, FUNCT_1:72 ;
:: thesis:

end;

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

then A115: e in EV1Xdb by A113, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) +* (EL | EV1Xdb)) . e = (EL | EV1Xdb) . e by A110, FUNCT_4:14
.= EL . e by A115, 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 A110, A112, FUNCT_1:72; :: thesis:

end;

then A116: (Sum (EL | (G .edgesDBetween V2,{(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) + (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})),{(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) = Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))})) by A107, A110, A111, FUNCT_1:9, GLIB_004:3;

now

let e be set ; :: thesis:

hereby :: thesis:

end;

end;

now

let e be set ; :: thesis:
assume e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2 ; :: thesis:
then e DSJoins {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2,G by GLIB_000:def 33;
then A124: ( e in the_Edges_of G & (the_Target_of G) . e in V2 & (the_Source_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} ) by GLIB_000:def 18;
then not (the_Target_of G) . e in {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A43, TARSKI:def 1;
then (the_Target_of G) . e in (the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))} by A124, XBOOLE_0:def 5;
then e DSJoins {(choose (((the_Vertices_of G) \ V2) \ {sink}))},(the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))},G by A124, 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;

now

let e be set ; :: thesis:
assume A128: 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 A129: 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 A130: 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 A126, FUNCT_4:12
.= EL . e by A130, FUNCT_1:72 ;
:: thesis:

end;

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

then A131: e in EXV1cb by A129, XBOOLE_0:def 5;
hence ((EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2)) +* (EL | EXV1cb)) . e = (EL | EXV1cb) . e by A126, FUNCT_4:14
.= EL . e by A131, 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 A126, A128, FUNCT_1:72; :: thesis:

end;

then A132: (Sum (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},V2))) + (Sum (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ (V2 \/ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))))) = Sum (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) by A123, A126, A127, FUNCT_1:9, GLIB_004:3;
reconsider x = choose (((the_Vertices_of G) \ V2) \ {sink}) as Vertex of G by A42;
( x .edgesIn() = G .edgesDBetween (the_Vertices_of G),{x} & x .edgesOut() = G .edgesDBetween {x},(the_Vertices_of G) ) by GLIB_000:42;
then A133: Sum (EL | (G .edgesDBetween (the_Vertices_of G),{x})) = Sum (EL | (G .edgesDBetween {x},(the_Vertices_of G))) by A1, A40, A43, A47, Def7;

now

let e be set ; :: thesis:

hereby :: thesis:

assume e in (G .edgesDBetween (the_Vertices_of G),{x}) \ (G .edgesDBetween {x},{x}) ; :: thesis:
then ( e in G .edgesDBetween (the_Vertices_of G),{x} & not e in G .edgesDBetween {x},{x} ) by XBOOLE_0:def 5;
then A134: ( e DSJoins the_Vertices_of G,{x},G & not e DSJoins {x},{x},G ) by GLIB_000:def 33;
then A135: ( e in the_Edges_of G & (the_Source_of G) . e in the_Vertices_of G & (the_Target_of G) . e in {x} ) by GLIB_000:def 18;
then not (the_Source_of G) . e in {x} by A134, GLIB_000:def 18;
then (the_Source_of G) . e in (the_Vertices_of G) \ {x} by A135, XBOOLE_0:def 5;
then e DSJoins (the_Vertices_of G) \ {x},{x},G by A135, 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 e in G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))} ; :: thesis:
then e DSJoins (the_Vertices_of G) \ {x},{x},G by GLIB_000:def 33;
then A136: ( e in the_Edges_of G & (the_Source_of G) . e in (the_Vertices_of G) \ {x} & (the_Target_of G) . e in {x} ) by GLIB_000:def 18;
then ( (the_Source_of G) . e in the_Vertices_of G & 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 A137: not e in G .edgesDBetween {x},{x} by GLIB_000:def 33;
e DSJoins the_Vertices_of G,{x},G by A136, 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 A137, XBOOLE_0:def 5; :: thesis:

end;

then A138: (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;
reconsider EXXfb = (G .edgesDBetween (the_Vertices_of G),{x}) \ (G .edgesDBetween {x},{x}) as Subset of (the_Edges_of G) ;
A139: ( dom (EL | (G .edgesDBetween (the_Vertices_of G),{x})) = G .edgesDBetween (the_Vertices_of G),{x} & dom (EL | (G .edgesDBetween {x},{x})) = G .edgesDBetween {x},{x} & dom (EL | EXXfb) = EXXfb ) by PARTFUN1:def 4;
then A140: dom ((EL | (G .edgesDBetween {x},{x})) +* (EL | EXXfb)) = (G .edgesDBetween {x},{x}) \/ EXXfb by FUNCT_4:def 1
.= (G .edgesDBetween {x},{x}) \/ (G .edgesDBetween (the_Vertices_of G),{x}) by XBOOLE_1:39
.= G .edgesDBetween (the_Vertices_of G),{x} by GLIB_000:41, XBOOLE_1:12 ;

now

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

now

per cases ;

suppose A142: 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 A139, FUNCT_4:12
.= EL . e by A142, FUNCT_1:72 ;
:: thesis:

end;

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

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

end;

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

end;

then A144: Sum (EL | (G .edgesDBetween (the_Vertices_of G),{x})) = (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}),{(choose (((the_Vertices_of G) \ V2) \ {sink}))}))) + (Sum (EL | (G .edgesDBetween {x},{x}))) by A138, A139, A140, FUNCT_1:9, GLIB_004:3;

now

let e be set ; :: thesis:

hereby :: thesis:

assume e in (G .edgesDBetween {x},(the_Vertices_of G)) \ (G .edgesDBetween {x},{x}) ; :: thesis:
then ( e in G .edgesDBetween {x},(the_Vertices_of G) & not e in G .edgesDBetween {x},{x} ) by XBOOLE_0:def 5;
then A145: ( e DSJoins {x}, the_Vertices_of G,G & not e DSJoins {x},{x},G ) by GLIB_000:def 33;
then A146: ( e in the_Edges_of G & (the_Target_of G) . e in the_Vertices_of G & (the_Source_of G) . e in {x} ) by GLIB_000:def 18;
then not (the_Target_of G) . e in {x} by A145, GLIB_000:def 18;
then (the_Target_of G) . e in (the_Vertices_of G) \ {x} by A146, XBOOLE_0:def 5;
then e DSJoins {x},(the_Vertices_of G) \ {x},G by A146, 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 e in G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))}) ; :: thesis:
then e DSJoins {x},(the_Vertices_of G) \ {x},G by GLIB_000:def 33;
then A147: ( e in the_Edges_of G & (the_Target_of G) . e in (the_Vertices_of G) \ {x} & (the_Source_of G) . e in {x} ) by GLIB_000:def 18;
then ( (the_Target_of G) . e in the_Vertices_of G & 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 A148: not e in G .edgesDBetween {x},{x} by GLIB_000:def 33;
e DSJoins {x}, the_Vertices_of G,G by A147, 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 A148, XBOOLE_0:def 5; :: thesis:

end;

now

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

now

per cases ;

suppose A153: 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 A150, FUNCT_4:12
.= EL . e by A153, FUNCT_1:72 ;
:: thesis:

end;

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

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

end;

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

end;

then Sum (EL | (G .edgesDBetween {x},(the_Vertices_of G))) = (Sum (EL | (G .edgesDBetween {(choose (((the_Vertices_of G) \ V2) \ {sink}))},((the_Vertices_of G) \ {(choose (((the_Vertices_of G) \ V2) \ {sink}))})))) + (Sum (EL | (G .edgesDBetween {x},{x}))) by A149, A150, A151, FUNCT_1:9, GLIB_004:3;
hence EL .flow source,sink = (Sum (EL | (G .edgesDBetween V2,((the_Vertices_of G) \ V2)))) - (Sum (EL | (G .edgesDBetween ((the_Vertices_of G) \ V2),V2))) by A48, A59, A71, A76, A89, A95, A100, A116, A132, A133, A144; :: thesis:

end;

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

end;

A155: for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A37, A38);
set n = card ((the_Vertices_of G) \ V);

now

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

end;

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 A1, A155; :: thesis: