let G be real-weighted WGraph; :: thesis: for EL being FF:ELabeling of
for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq EL,source) . n) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . n) )
let EL be FF:ELabeling of ; :: thesis: for source being Vertex of G
for n being Nat
for v being set st v in dom ((AP:CompSeq EL,source) . n) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . n) )
let source be Vertex of G; :: thesis: for n being Nat
for v being set st v in dom ((AP:CompSeq EL,source) . n) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . n) )
set CS = AP:CompSeq EL,source;
set G0 = (AP:CompSeq EL,source) . 0 ;
defpred S₁[ Nat] means for v being set st v in dom ((AP:CompSeq EL,source) . $1) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . $1) );

now

let v be set ; :: thesis: ( v in dom ((AP:CompSeq EL,source) . 0 ) implies ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . 0 ) ) )
assume A1: v in dom ((AP:CompSeq EL,source) . 0 ) ; :: thesis: ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . 0 ) )
then reconsider v' = v as Vertex of G ;
set P = G .walkOf v';
take P = G .walkOf v'; :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . 0 ) )
thus P is_augmenting_wrt EL by Th001; :: thesis: ( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . 0 ) )
v in {source} by A1, Th3;
then v = source by TARSKI:def 1;
hence P is_Walk_from source,v by GLIB_001:14; :: thesis: P .vertices() c= dom ((AP:CompSeq EL,source) . 0 )
P .vertices() = {v'} by GLIB_001:91;
hence P .vertices() c= dom ((AP:CompSeq EL,source) . 0 ) by A1, ZFMISC_1:37; :: thesis: verum

end;

then A2: S₁[ 0 ] ;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
set Gn = (AP:CompSeq EL,source) . n;
set Gn1 = (AP:CompSeq EL,source) . (n + 1);
set Next = AP:NextBestEdges ((AP:CompSeq EL,source) . n);
set e = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n));
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: (AP:CompSeq EL,source) . (n + 1) = AP:Step ((AP:CompSeq EL,source) . n) by Def15;

now

per cases ( AP:NextBestEdges ((AP:CompSeq EL,source) . n) = {} or AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} ) ;

suppose AP:NextBestEdges ((AP:CompSeq EL,source) . n) = {} ; :: thesis: S₁[n + 1]

then (AP:CompSeq EL,source) . (n + 1) = (AP:CompSeq EL,source) . n by A5, Def14;
hence S₁[n + 1] by A4; :: thesis: verum

end;

suppose A6: AP:NextBestEdges ((AP:CompSeq EL,source) . n) <> {} ; :: thesis: S₁[n + 1]

set se = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)));
set te = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)));

now

per cases ( choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_forward_edge_wrt (AP:CompSeq EL,source) . n or choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_backward_edge_wrt (AP:CompSeq EL,source) . n ) by A6, Def13;

suppose A7: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_forward_edge_wrt (AP:CompSeq EL,source) . n ; :: thesis: for v being set st v in dom ((AP:CompSeq EL,source) . (n + 1)) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

then A8: ( choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) in the_Edges_of G & (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) & not (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) & EL . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) < (the_Weight_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) ) by Def10;
then (AP:CompSeq EL,source) . (n + 1) = ((AP:CompSeq EL,source) . n) +* (((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))) by A5, A6, Def14;
then A9: dom ((AP:CompSeq EL,source) . (n + 1)) = (dom ((AP:CompSeq EL,source) . n)) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by Tw0;
then A10: dom ((AP:CompSeq EL,source) . n) c= dom ((AP:CompSeq EL,source) . (n + 1)) by XBOOLE_1:7;
(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by TARSKI:def 1;
then A11: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . (n + 1)) by A9, XBOOLE_0:def 3;
A12: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . (n + 1)) by A8, A10;
let v be set ; :: thesis: ( v in dom ((AP:CompSeq EL,source) . (n + 1)) implies ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) )
assume A13: v in dom ((AP:CompSeq EL,source) . (n + 1)) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
A15: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) DJoins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),G by A8, GLIB_000:def 16;

now

per cases ( v in dom ((AP:CompSeq EL,source) . n) or v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ) by A9, A13, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq EL,source) . n) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

then consider P being Path of G such that
A16: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . n) ) by A4;
take P = P; :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) by A10, A16, XBOOLE_1:1; :: thesis: verum

end;

suppose v in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

then A17: v = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by TARSKI:def 1;

now

per cases ( (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) = source or (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) <> source ) ;

suppose A18: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) = source ; :: thesis: ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

set P = G .walkOf ((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))));
A19: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),G by A8, GLIB_000:def 15;
take P = G .walkOf ((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))); :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

now

let n be odd Nat; :: thesis: ( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) ) )
assume n < len P ; :: thesis: ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )
then n < 2 + 1 by A19, GLIB_001:15;
then n <= 2 * 1 by NAT_1:13;
then n < 1 + 1 by XXREAL_0:1;
then ( 1 <= n & n <= 1 ) by HEYTING3:1, NAT_1:13;
then A20: n = 1 by XXREAL_0:1;
P = <*((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))*> by A19, GLIB_001:def 5;
then A21: ( P . n = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) & P . (n + 1) = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) & P . (n + 2) = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) ) by A20, FINSEQ_1:62;
thus ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) by A7, A21, Def10; :: thesis: ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) )
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: 0 < EL . (P . (n + 1))
hence 0 < EL . (P . (n + 1)) by A21, A8, GLIB_000:def 16; :: thesis: verum

end;

hence P is_augmenting_wrt EL by Def12; :: thesis: ( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus P is_Walk_from source,v by A17, A18, A19, GLIB_001:16; :: thesis: P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1))

now

let x be set ; :: thesis: ( x in P .vertices() implies x in dom ((AP:CompSeq EL,source) . (n + 1)) )
assume x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))
then x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by A19, GLIB_001:92;
hence x in dom ((AP:CompSeq EL,source) . (n + 1)) by A11, A12, TARSKI:def 2; :: thesis: verum

end;

hence P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

suppose A23: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) <> source ; :: thesis: ex P2 being Path of G st
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

consider P being Path of G such that
A24: ( P is_augmenting_wrt EL & P is_Walk_from source,(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) & P .vertices() c= dom ((AP:CompSeq EL,source) . n) ) by A4, A8;
set P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)));
A25: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),v,G by A8, A17, GLIB_000:def 15;
A26: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) = P .last() by A24, GLIB_001:def 23;
then P .first() <> P .last() by A23, A24, GLIB_001:def 23;
then A27: not P is closed by GLIB_001:def 24;
A28: not v in P .vertices() by A7, A17, A24, Def10;
then reconsider P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) as Path of G by A25, A26, A27, GLIB_001:152;
take P2 = P2; :: thesis: ( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus P2 is_augmenting_wrt EL by A8, A15, A17, A24, A26, A28, Th2; :: thesis: ( P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus P2 is_Walk_from source,v by A24, A25, GLIB_001:67; :: thesis: P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1))

now

let x be set ; :: thesis: ( x in P2 .vertices() implies x in dom ((AP:CompSeq EL,source) . (n + 1)) )
assume x in P2 .vertices() ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))
then A29: x in (P .vertices() ) \/ {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by A17, A25, A26, GLIB_001:96;

now

per cases ( x in P .vertices() or x in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ) by A29, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))

then x in dom ((AP:CompSeq EL,source) . n) by A24;
hence x in dom ((AP:CompSeq EL,source) . (n + 1)) by A10; :: thesis: verum

end;

suppose x in {((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))

hence x in dom ((AP:CompSeq EL,source) . (n + 1)) by A9, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in dom ((AP:CompSeq EL,source) . (n + 1)) ; :: thesis: verum

end;

hence P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) ; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) ; :: thesis: verum

end;

suppose A30: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) is_backward_edge_wrt (AP:CompSeq EL,source) . n ; :: thesis: for v being set st v in dom ((AP:CompSeq EL,source) . (n + 1)) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

then A31: ( choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) in the_Edges_of G & (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) & not (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . n) & 0 < EL . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) ) by Def11;
then (AP:CompSeq EL,source) . (n + 1) = ((AP:CompSeq EL,source) . n) +* (((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))) .--> (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))) by A5, A6, Def14;
then A32: dom ((AP:CompSeq EL,source) . (n + 1)) = (dom ((AP:CompSeq EL,source) . n)) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by Tw0;
then A33: dom ((AP:CompSeq EL,source) . n) c= dom ((AP:CompSeq EL,source) . (n + 1)) by XBOOLE_1:7;
(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by TARSKI:def 1;
then A34: (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . (n + 1)) by A32, XBOOLE_0:def 3;
A35: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) in dom ((AP:CompSeq EL,source) . (n + 1)) by A31, A33;
let v be set ; :: thesis: ( v in dom ((AP:CompSeq EL,source) . (n + 1)) implies ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) )
assume A36: v in dom ((AP:CompSeq EL,source) . (n + 1)) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
A38: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) DJoins (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),G by A31, GLIB_000:def 16;

now

per cases ( v in dom ((AP:CompSeq EL,source) . n) or v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ) by A32, A36, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq EL,source) . n) ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

then consider P being Path of G such that
A39: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . n) ) by A4;
take P = P; :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) by A33, A39, XBOOLE_1:1; :: thesis: verum

end;

suppose v in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ; :: thesis: ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

then A40: v = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) by TARSKI:def 1;

now

per cases ( (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) = source or (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) <> source ) ;

suppose A41: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) = source ; :: thesis: ex P being Walk of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

set P = G .walkOf ((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))));
take P = G .walkOf ((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))); :: thesis: ( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
A42: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),(the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),G by A31, GLIB_000:def 15;

now

let n be odd Nat; :: thesis: ( n < len P implies ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) ) )
assume n < len P ; :: thesis: ( ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) & ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) ) )
then n < 2 + 1 by A42, GLIB_001:15;
then n <= 2 * 1 by NAT_1:13;
then n < 1 + 1 by XXREAL_0:1;
then ( 1 <= n & n <= 1 ) by HEYTING3:1, NAT_1:13;
then A43: n = 1 by XXREAL_0:1;
P = <*((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),(choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))*> by A42, GLIB_001:def 5;
then A44: ( P . n = (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) & P . (n + 1) = choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) & P . (n + 2) = (the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) ) by A43, FINSEQ_1:62;
thus ( P . (n + 1) DJoins P . n,P . (n + 2),G implies EL . (P . (n + 1)) < (the_Weight_of G) . (P . (n + 1)) ) by A44, A31, GLIB_000:def 16; :: thesis: ( not P . (n + 1) DJoins P . n,P . (n + 2),G implies 0 < EL . (P . (n + 1)) )
assume not P . (n + 1) DJoins P . n,P . (n + 2),G ; :: thesis: 0 < EL . (P . (n + 1))
thus 0 < EL . (P . (n + 1)) by A30, A44, Def11; :: thesis: verum

end;

hence P is_augmenting_wrt EL by Def12; :: thesis: ( P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus P is_Walk_from source,v by A40, A41, A42, GLIB_001:16; :: thesis: P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1))

now

let x be set ; :: thesis: ( x in P .vertices() implies x in dom ((AP:CompSeq EL,source) . (n + 1)) )
assume x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))
then x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)))),((the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by A42, GLIB_001:92;
hence x in dom ((AP:CompSeq EL,source) . (n + 1)) by A34, A35, TARSKI:def 2; :: thesis: verum

end;

hence P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

suppose A45: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) <> source ; :: thesis: ex P2 being Path of G st
( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )

consider P being Path of G such that
A46: ( P is_augmenting_wrt EL & P is_Walk_from source,(the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) & P .vertices() c= dom ((AP:CompSeq EL,source) . n) ) by A4, A31;
set P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)));
A47: choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n)) Joins (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))),v,G by A31, A40, GLIB_000:def 15;
A48: (the_Target_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) = P .last() by A46, GLIB_001:def 23;
then P .first() <> P .last() by A45, A46, GLIB_001:def 23;
then A49: not P is closed by GLIB_001:def 24;
A50: not v in P .vertices() by A30, A40, A46, Def11;
then reconsider P2 = P .addEdge (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))) as Path of G by A47, A48, A49, GLIB_001:152;
take P2 = P2; :: thesis: ( P2 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus P2 is_augmenting_wrt EL by A31, A38, A40, A46, A48, A50, Th2; :: thesis: ( P2 is_Walk_from source,v & P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) )
thus P2 is_Walk_from source,v by A46, A47, GLIB_001:67; :: thesis: P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1))

now

let x be set ; :: thesis: ( x in P2 .vertices() implies x in dom ((AP:CompSeq EL,source) . (n + 1)) )
assume x in P2 .vertices() ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))
then A51: x in (P .vertices() ) \/ {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} by A40, A47, A48, GLIB_001:96;

now

per cases ( x in P .vertices() or x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ) by A51, XBOOLE_0:def 3;

suppose x in P .vertices() ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))

then x in dom ((AP:CompSeq EL,source) . n) by A46;
hence x in dom ((AP:CompSeq EL,source) . (n + 1)) by A33; :: thesis: verum

end;

suppose x in {((the_Source_of G) . (choose (AP:NextBestEdges ((AP:CompSeq EL,source) . n))))} ; :: thesis: x in dom ((AP:CompSeq EL,source) . (n + 1))

hence x in dom ((AP:CompSeq EL,source) . (n + 1)) by A32, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in dom ((AP:CompSeq EL,source) . (n + 1)) ; :: thesis: verum

end;

hence P2 .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) ; :: thesis: verum

end;

end;

end;

hence ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . (n + 1)) ) ; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for n being Nat
for v being set st v in dom ((AP:CompSeq EL,source) . n) holds
ex P being Path of G st
( P is_augmenting_wrt EL & P is_Walk_from source,v & P .vertices() c= dom ((AP:CompSeq EL,source) . n) ) ; :: thesis: verum