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

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:13; :: 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

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:72
.= 0 by A1, A2, FUNCOP_1:13 ;
hence (EmptyBag (v .edgesOut() )) . e = (((FF:CompSeq G,source,sink) . 0 ) | (v .edgesOut() )) . e by PRE_POLY:52; :: 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:13 ;
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

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:72
.= 0 by A1, A4, FUNCOP_1:13 ;
hence (EmptyBag (v .edgesIn() )) . e = (((FF:CompSeq G,source,sink) . 0 ) | (v .edgesIn() )) . e by PRE_POLY:52; :: thesis: verum

end;

then Sum (((FF:CompSeq G,source,sink) . 0 ) | (v .edgesIn() )) = Sum (EmptyBag (v .edgesIn() )) by GLIB_004:6
.= 0 by UPROOTS:13 ;
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

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

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