set CS = AP:CompSeq (EL,source);
set FAP = AP:FindAugPath (EL,source);
defpred S₁[ Nat] means for v being set st v in dom ((AP:CompSeq (EL,source)) . $1) holds
ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . $1) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) );

now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A1: S₁[n] ; :: thesis: 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 = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A2: (AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n) by Def12;

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

per cases ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) or ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((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 A2, Def10;
hence S₁[n + 1] by A1; :: thesis: verum

end;

suppose A3: ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) ; :: thesis: S₁[n + 1]

then A4: ( the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n ) by Def9;
then A5: 0 < EL . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A3;
A6: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A3;
A7: (AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) by A2, A3, Def10;
then A8: dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} by Lm1;
A9: (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) by A3, A4;

now :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) holds
ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . (n + 1)) implies ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) )
assume A10: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

now :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

per cases ( v in dom ((AP:CompSeq (EL,source)) . n) or v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ) by A8, A10, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

then consider P being vertex-distinct Path of G such that
A11: P is_Walk_from source,v and
A12: P is_augmenting_wrt EL and
A13: P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) and
A14: for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) by A1;
take P = P; :: thesis: ( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by Th5, NAT_1:11;
hence ( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) by A11, A12, A13, A14; :: thesis: verum

end;

suppose A15: v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

then A16: v = (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by TARSKI:def 1;

now :: thesis: ex W2 being vertex-distinct Walk of G st
( W2 is_Walk_from source,v & W2 is_augmenting_wrt EL & W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )

consider W being vertex-distinct Path of G such that
A17: W is_Walk_from source,(the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) and
A18: W is_augmenting_wrt EL and
A19: W .vertices() c= dom ((AP:CompSeq (EL,source)) . n) and
A20: for n being even Nat st n in dom W holds
W . n = (AP:FindAugPath (EL,source)) . (W . (n + 1)) by A1, A9;
set W2 = W .addEdge the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A21: W .last() = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A17, GLIB_001:def 23;
then A22: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins W .last() ,(the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),G by A6;
A23: not (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in W .vertices() by A3, A19;
then reconsider W2 = W .addEdge the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) as vertex-distinct Walk of G by A22, GLIB_001:155;
take W2 = W2; :: thesis: ( W2 is_Walk_from source,v & W2 is_augmenting_wrt EL & W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )
W .first() = source by A17, GLIB_001:def 23;
hence W2 is_Walk_from source,v by A16, A22, GLIB_001:63; :: thesis: ( W2 is_augmenting_wrt EL & W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )
the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) DJoins (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),W .last() ,G by A6, A21;
hence W2 is_augmenting_wrt EL by A5, A18, A23, Th3; :: thesis: ( W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )
A24: W2 .vertices() = (W .vertices()) \/ {v} by A16, A22, GLIB_001:95;

now :: thesis: for x being object st x in W2 .vertices() holds
x in dom ((AP:CompSeq (EL,source)) . (n + 1))

let x be object ; :: thesis: ( x in W2 .vertices() implies x in dom ((AP:CompSeq (EL,source)) . (n + 1)) )
assume A25: x in W2 .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))

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

per cases ( x in W .vertices() or x in {v} ) by A24, A25, XBOOLE_0:def 3;

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

A27: dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by Th5, NAT_1:11;
x in dom ((AP:CompSeq (EL,source)) . n) by A19, A26;
hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A27; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))
let n be even Nat; :: thesis: ( n in dom W2 implies W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) )
assume A28: n in dom W2 ; :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))
then A29: n <= len W2 by FINSEQ_3:25;
A30: 1 <= n by A28, FINSEQ_3:25;

now :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))

per cases ( n <= len W or n > len W ) ;

suppose A31: n <= len W ; :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))

then n < len W by XXREAL_0:1;
then A32: n + 1 <= len W by NAT_1:13;
1 <= 1 + n by NAT_1:11;
then n + 1 in dom W by A32, FINSEQ_3:25;
then A33: W2 . (n + 1) = W . (n + 1) by A22, GLIB_001:65;
A34: n in dom W by A30, A31, FINSEQ_3:25;
then W2 . n = W . n by A22, GLIB_001:65;
hence W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) by A20, A34, A33; :: thesis: verum

end;

suppose A35: n > len W ; :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))

n <= (len W) + (2 * 1) by A22, A29, GLIB_001:64;
then n < ((len W) + 1) + 1 by XXREAL_0:1;
then A36: n <= (len W) + 1 by NAT_1:13;
(len W) + 1 <= n by A35, NAT_1:13;
then A37: n = (len W) + 1 by A36, XXREAL_0:1;
then A38: W2 . n = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A22, GLIB_001:65;
n + 1 = (len W) + (1 + 1) by A37;
then A39: W2 . (n + 1) = v by A16, A22, GLIB_001:65;
A40: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A8, A15, XBOOLE_0:def 3;
((AP:CompSeq (EL,source)) . (n + 1)) . v = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A7, A16, Lm3;
hence W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) by A38, A39, A40, Th7; :: thesis: verum

end;

end;

end;

hence W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ; :: thesis: verum

end;

hence ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) ; :: thesis: verum

end;

end;

end;

hence ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) ; :: thesis: verum

end;

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

end;

suppose A41: ( AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) <> {} & (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in dom ((AP:CompSeq (EL,source)) . n) ) ; :: thesis: S₁[n + 1]

then A42: (AP:CompSeq (EL,source)) . (n + 1) = ((AP:CompSeq (EL,source)) . n) +* (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) .--> the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)) by A2, Def10;
then A43: dom ((AP:CompSeq (EL,source)) . (n + 1)) = (dom ((AP:CompSeq (EL,source)) . n)) \/ {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} by Lm1;
A44: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A41;
A45: ( the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_forward_edge_wrt (AP:CompSeq (EL,source)) . n or the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) is_backward_edge_wrt (AP:CompSeq (EL,source)) . n ) by A41, Def9;
then A46: EL . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) < (the_Weight_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A41;

now :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . (n + 1)) holds
ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . (n + 1)) implies ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) )
assume A47: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

now :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

per cases ( v in dom ((AP:CompSeq (EL,source)) . n) or v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ) by A43, A47, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

then consider P being vertex-distinct Path of G such that
A48: P is_Walk_from source,v and
A49: P is_augmenting_wrt EL and
A50: P .vertices() c= dom ((AP:CompSeq (EL,source)) . n) and
A51: for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) by A1;
take P = P; :: thesis: ( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )
dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by Th5, NAT_1:11;
hence ( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) by A48, A49, A50, A51; :: thesis: verum

end;

suppose A52: v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis: ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

then A53: v = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by TARSKI:def 1;

now :: thesis: ex W2 being vertex-distinct Walk of G st
( W2 is_Walk_from source,v & W2 is_augmenting_wrt EL & W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )

consider W being vertex-distinct Path of G such that
A54: W is_Walk_from source,(the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) and
A55: W is_augmenting_wrt EL and
A56: W .vertices() c= dom ((AP:CompSeq (EL,source)) . n) and
A57: for n being even Nat st n in dom W holds
W . n = (AP:FindAugPath (EL,source)) . (W . (n + 1)) by A1, A41;
set W2 = W .addEdge the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n);
A58: W .last() = (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A54, GLIB_001:def 23;
then A59: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins W .last() ,(the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),G by A44;
A60: not (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) in W .vertices() by A41, A45, A56;
then reconsider W2 = W .addEdge the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) as vertex-distinct Walk of G by A59, GLIB_001:155;
take W2 = W2; :: thesis: ( W2 is_Walk_from source,v & W2 is_augmenting_wrt EL & W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )
W .first() = source by A54, GLIB_001:def 23;
hence W2 is_Walk_from source,v by A53, A59, GLIB_001:63; :: thesis: ( W2 is_augmenting_wrt EL & W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )
the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) DJoins W .last() ,(the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),G by A44, A58;
hence W2 is_augmenting_wrt EL by A46, A55, A60, Th3; :: thesis: ( W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ) )
A61: W2 .vertices() = (W .vertices()) \/ {v} by A53, A59, GLIB_001:95;

now :: thesis: for x being object st x in W2 .vertices() holds
x in dom ((AP:CompSeq (EL,source)) . (n + 1))

let x be object ; :: thesis: ( x in W2 .vertices() implies x in dom ((AP:CompSeq (EL,source)) . (n + 1)) )
assume A62: x in W2 .vertices() ; :: thesis: x in dom ((AP:CompSeq (EL,source)) . (n + 1))

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

per cases ( x in W .vertices() or x in {v} ) by A61, A62, XBOOLE_0:def 3;

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

A64: dom ((AP:CompSeq (EL,source)) . n) c= dom ((AP:CompSeq (EL,source)) . (n + 1)) by Th5, NAT_1:11;
x in dom ((AP:CompSeq (EL,source)) . n) by A56, A63;
hence x in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A64; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence W2 .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) ; :: thesis: for n being even Nat st n in dom W2 holds
W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))
let n be even Nat; :: thesis: ( n in dom W2 implies W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) )
assume A65: n in dom W2 ; :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))
then A66: n <= len W2 by FINSEQ_3:25;
A67: 1 <= n by A65, FINSEQ_3:25;

now :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))

per cases ( n <= len W or n > len W ) ;

suppose A68: n <= len W ; :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))

then n < len W by XXREAL_0:1;
then A69: n + 1 <= len W by NAT_1:13;
1 <= 1 + n by NAT_1:11;
then n + 1 in dom W by A69, FINSEQ_3:25;
then A70: W2 . (n + 1) = W . (n + 1) by A59, GLIB_001:65;
A71: n in dom W by A67, A68, FINSEQ_3:25;
then W2 . n = W . n by A59, GLIB_001:65;
hence W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) by A57, A71, A70; :: thesis: verum

end;

suppose A72: n > len W ; :: thesis: W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1))

n <= (len W) + (2 * 1) by A59, A66, GLIB_001:64;
then n < ((len W) + 1) + 1 by XXREAL_0:1;
then A73: n <= (len W) + 1 by NAT_1:13;
(len W) + 1 <= n by A72, NAT_1:13;
then A74: n = (len W) + 1 by A73, XXREAL_0:1;
then A75: W2 . n = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A59, GLIB_001:65;
n + 1 = (len W) + (1 + 1) by A74;
then A76: W2 . (n + 1) = v by A53, A59, GLIB_001:65;
A77: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) by A43, A52, XBOOLE_0:def 3;
((AP:CompSeq (EL,source)) . (n + 1)) . v = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A42, A53, Lm3;
hence W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) by A75, A76, A77, Th7; :: thesis: verum

end;

end;

end;

hence W2 . n = (AP:FindAugPath (EL,source)) . (W2 . (n + 1)) ; :: thesis: verum

end;

hence ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) ; :: thesis: verum

end;

end;

end;

hence ex P being vertex-distinct Path of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . (n + 1)) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) ; :: thesis: verum

end;

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

end;

end;

end;

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

end;

then A78: for n being Nat st S₁[n] holds
S₁[n + 1] ;

now :: thesis: for v being set st v in dom ((AP:CompSeq (EL,source)) . 0) holds
ex P being Walk of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )

set P = G .walkOf source;
let v be set ; :: thesis: ( v in dom ((AP:CompSeq (EL,source)) . 0) implies ex P being Walk of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) ) )
assume A79: v in dom ((AP:CompSeq (EL,source)) . 0) ; :: thesis: ex P being Walk of G st
( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )
take P = G .walkOf source; :: thesis: ( P is_Walk_from source,v & P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )
v in {source} by A79, Th4;
then v = source by TARSKI:def 1;
hence P is_Walk_from source,v by GLIB_001:13; :: thesis: ( P is_augmenting_wrt EL & P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )
thus P is_augmenting_wrt EL by Th1; :: thesis: ( P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) & ( for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) ) )
P .vertices() = {source} by GLIB_001:90;
hence P .vertices() c= dom ((AP:CompSeq (EL,source)) . 0) by Th4; :: thesis: for n being even Nat st n in dom P holds
P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1))
let n be even Nat; :: thesis: ( n in dom P implies P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) )
assume A80: n in dom P ; :: thesis: P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1))
then n <= len P by FINSEQ_3:25;
then A81: n < len P by XXREAL_0:1;
1 <= n by A80, FINSEQ_3:25;
hence P . n = (AP:FindAugPath (EL,source)) . (P . (n + 1)) by A81, GLIB_001:13; :: thesis: verum

end;

then A82: S₁[ 0 ] ;
A83: for n being Nat holds S₁[n] from NAT_1:sch 2(A82, A78);

hereby :: thesis: ( not sink in dom (AP:FindAugPath (EL,source)) implies ex b₁ being vertex-distinct Path of G st b₁ = G .walkOf source )

assume sink in dom (AP:FindAugPath (EL,source)) ; :: thesis: ex W being vertex-distinct Path of G st
( W is_Walk_from source,sink & W is_augmenting_wrt EL & ( for n being even Nat st n in dom W holds
W . n = (AP:FindAugPath (EL,source)) . (W . (n + 1)) ) )
then consider W being vertex-distinct Path of G such that
A84: W is_Walk_from source,sink and
A85: W is_augmenting_wrt EL and
W .vertices() c= dom (AP:FindAugPath (EL,source)) and
A86: for n being even Nat st n in dom W holds
W . n = (AP:FindAugPath (EL,source)) . (W . (n + 1)) by A83;
take W = W; :: thesis: ( W is_Walk_from source,sink & W is_augmenting_wrt EL & ( for n being even Nat st n in dom W holds
W . n = (AP:FindAugPath (EL,source)) . (W . (n + 1)) ) )
thus ( W is_Walk_from source,sink & W is_augmenting_wrt EL & ( for n being even Nat st n in dom W holds
W . n = (AP:FindAugPath (EL,source)) . (W . (n + 1)) ) ) by A84, A85, A86; :: thesis: verum

end;

thus ( not sink in dom (AP:FindAugPath (EL,source)) implies ex b₁ being vertex-distinct Path of G st b₁ = G .walkOf source ) ; :: thesis: verum