let G be _finite natural-weighted WGraph; :: thesis: for source, sink being Vertex of G
for n being Nat st source <> sink holds
(FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink
let source, sink be Vertex of G; :: thesis: for n being Nat st source <> sink holds
(FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink
let n be Nat; :: thesis: ( source <> sink implies (FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink )
set CS = FF:CompSeq (G,source,sink);
defpred S₁[ Nat] means (FF:CompSeq (G,source,sink)) . $1 has_valid_flow_from source,sink;

now :: thesis: ( ( for e being set st e in the_Edges_of G holds
( 0 <= ((FF:CompSeq (G,source,sink)) . 0) . e & ((FF:CompSeq (G,source,sink)) . 0) . e <= (the_Weight_of G) . e ) ) & ( for v being Vertex of G st v <> source & v <> sink holds
Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) = Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) ) )

set G0 = (FF:CompSeq (G,source,sink)) . 0;
A1: (FF:CompSeq (G,source,sink)) . 0 = (the_Edges_of G) --> 0 by Def20;
hence for e being set st e in the_Edges_of G holds
( 0 <= ((FF:CompSeq (G,source,sink)) . 0) . e & ((FF:CompSeq (G,source,sink)) . 0) . e <= (the_Weight_of G) . e ) by FUNCOP_1:7; :: thesis: for v being Vertex of G st v <> source & v <> sink holds
Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) = Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut()))
let v be Vertex of G; :: thesis: ( v <> source & v <> sink implies Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) = Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) )
set B1 = EmptyBag (v .edgesIn());
set B2 = EmptyBag (v .edgesOut());
set E1 = ((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn());
set E2 = ((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut());

now :: thesis: for e being set st e in v .edgesOut() holds
(EmptyBag (v .edgesOut())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) . e

let e be set ; :: thesis: ( e in v .edgesOut() implies (EmptyBag (v .edgesOut())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) . e )
assume A2: e in v .edgesOut() ; :: thesis: (EmptyBag (v .edgesOut())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) . e
then (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) . e = ((FF:CompSeq (G,source,sink)) . 0) . e by FUNCT_1:49
.= 0 by A1, A2, FUNCOP_1:7 ;
hence (EmptyBag (v .edgesOut())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) . e by PBOOLE:5; :: thesis: verum

end;

then A3: Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) = Sum (EmptyBag (v .edgesOut())) by GLIB_004:6
.= 0 by UPROOTS:11 ;
assume that
v <> source and
v <> sink ; :: thesis: Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) = Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut()))

now :: thesis: for e being set st e in v .edgesIn() holds
(EmptyBag (v .edgesIn())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) . e

let e be set ; :: thesis: ( e in v .edgesIn() implies (EmptyBag (v .edgesIn())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) . e )
assume A4: e in v .edgesIn() ; :: thesis: (EmptyBag (v .edgesIn())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) . e
then (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) . e = ((FF:CompSeq (G,source,sink)) . 0) . e by FUNCT_1:49
.= 0 by A1, A4, FUNCOP_1:7 ;
hence (EmptyBag (v .edgesIn())) . e = (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) . e by PBOOLE:5; :: thesis: verum

end;

then Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) = Sum (EmptyBag (v .edgesIn())) by GLIB_004:6
.= 0 by UPROOTS:11 ;
hence Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesIn())) = Sum (((FF:CompSeq (G,source,sink)) . 0) | (v .edgesOut())) by A3; :: thesis: verum

end;

then A5: S₁[ 0 ] by Def2;
assume A6: source <> sink ; :: thesis: (FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink

now :: thesis: for n being Nat st (FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink holds
S₁[n + 1]

let n be Nat; :: thesis: ( (FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink implies S₁[n + 1] )
set Gn = (FF:CompSeq (G,source,sink)) . n;
set Gn1 = (FF:CompSeq (G,source,sink)) . (n + 1);
assume A7: (FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink ; :: thesis: S₁[n + 1]
A8: (FF:CompSeq (G,source,sink)) . (n + 1) = FF:Step (((FF:CompSeq (G,source,sink)) . n),source,sink) by Def20;

now :: thesis: S₁[n + 1]

per cases ( sink in dom (AP:FindAugPath (((FF:CompSeq (G,source,sink)) . n),source)) or not sink in dom (AP:FindAugPath (((FF:CompSeq (G,source,sink)) . n),source)) ) ;

suppose A9: sink in dom (AP:FindAugPath (((FF:CompSeq (G,source,sink)) . n),source)) ; :: thesis: S₁[n + 1]

set P = AP:GetAugPath (((FF:CompSeq (G,source,sink)) . n),source,sink);
A10: AP:GetAugPath (((FF:CompSeq (G,source,sink)) . n),source,sink) is_Walk_from source,sink by A9, Def14;
A11: AP:GetAugPath (((FF:CompSeq (G,source,sink)) . n),source,sink) is_augmenting_wrt (FF:CompSeq (G,source,sink)) . n by A9, Def14;
(FF:CompSeq (G,source,sink)) . (n + 1) = FF:PushFlow (((FF:CompSeq (G,source,sink)) . n),(AP:GetAugPath (((FF:CompSeq (G,source,sink)) . n),source,sink))) by A8, A9, Def18;
hence S₁[n + 1] by A6, A7, A10, A11, Th14; :: thesis: verum

end;

suppose not sink in dom (AP:FindAugPath (((FF:CompSeq (G,source,sink)) . n),source)) ; :: thesis: S₁[n + 1]

hence S₁[n + 1] by A7, A8, Def18; :: thesis: verum

end;

end;

end;

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

end;

then A12: for n being Nat st S₁[n] holds
S₁[n + 1] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A12);
hence (FF:CompSeq (G,source,sink)) . n has_valid_flow_from source,sink ; :: thesis: verum