set FAP = AP:FindAugPath (EL,source);
set CS = AP:CompSeq (EL,source);
let IT1, IT2 be vertex-distinct Path of G; :: thesis:
defpred S₁[ Nat] means for v being set
for P1, P2 being vertex-distinct Path of G st v in dom ((AP:CompSeq (EL,source)) . $1) & P1 is_Walk_from source,v & P1 is_augmenting_wrt EL & P2 is_Walk_from source,v & P2 is_augmenting_wrt EL & ( for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) ) & ( for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ) holds
P1 = P2;
set G0 = (AP:CompSeq (EL,source)) . 0;

let n be Nat; :: thesis:
assume A87: S₁[n] ; :: thesis:
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);
A88: (AP:CompSeq (EL,source)) . (n + 1) = AP:Step ((AP:CompSeq (EL,source)) . n) by Def12;

per cases ;

suppose AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) = {} ; :: thesis:

then (AP:CompSeq (EL,source)) . (n + 1) = (AP:CompSeq (EL,source)) . n by A88, Def10;
hence S₁[n + 1] by A87; :: thesis:

end;

suppose A89: ( 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:

now :: thesis:

let v be set ; :: thesis:
let P1, P2 be vertex-distinct Path of G; :: thesis:
assume that
A95: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) and
A96: P1 is_Walk_from source,v and
A97: P1 is_augmenting_wrt EL and
A98: P2 is_Walk_from source,v and
A99: P2 is_augmenting_wrt EL and
A100: for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) and
A101: for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ; :: thesis:
A102: P1 . (len P1) = v by A96, GLIB_001:17;
A103: P2 . 1 = source by A98, GLIB_001:17;
A104: P2 . (len P2) = v by A98, GLIB_001:17;
A105: P1 . 1 = source by A96, GLIB_001:17;

now :: thesis:

per cases by A94, A95, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis:

hence P1 = P2 by A87, A96, A97, A98, A99, A100, A101; :: thesis:

end;

suppose A106: v in {((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis:

then A107: v = (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by TARSKI:def 1;
then ((AP:CompSeq (EL,source)) . (n + 1)) . v = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A93, Lm3;
then A108: (AP:FindAugPath (EL,source)) . v = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A95, Th7;
A109: v <> source by A89, A91, A106, TARSKI:def 1;
then P1 . 1 <> P1 .last() by A105, A102, GLIB_001:def 7;
then P1 .first() <> P1 .last() by GLIB_001:def 6;
then P1 is trivial by GLIB_001:127;
then A110: 3 <= len P1 by GLIB_001:125;
P2 . 1 <> P2 .last() by A103, A104, A109, GLIB_001:def 7;
then P2 .first() <> P2 .last() by GLIB_001:def 6;
then P2 is trivial by GLIB_001:127;
then A111: 3 <= len P2 by GLIB_001:125;
then A112: 3 - 2 < (len P2) - 0 by XREAL_1:15;
3 - 2 < (len P1) - 0 by A110, XREAL_1:15;
then reconsider lenP11 = (len P1) - 1, lenP21 = (len P2) - 1 as even Element of NAT by A112, INT_1:5;
A113: lenP11 < (len P1) - 0 by XREAL_1:15;
3 - 2 <= lenP11 by A110, XREAL_1:15;
then A114: lenP11 in dom P1 by A113, FINSEQ_3:25;
lenP11 + 1 = len P1 ;
then A115: P1 . lenP11 = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A100, A102, A114, A108;
then consider lenP12 being odd Element of NAT such that
A116: lenP12 = lenP11 - 1 and
lenP11 - 1 in dom P1 and
lenP11 + 1 in dom P1 and
A117: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins P1 . lenP12,v,G by A102, A114, GLIB_001:9;
A118: P1 . lenP12 = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A107, A117;
set P1A = P1 .cut (((2 * 0) + 1),lenP12);
A119: lenP12 < len P1 by A113, A116, XREAL_1:15;

A120: now :: thesis:

let n be even Nat; :: thesis:
assume A121: n in dom (P1 .cut (((2 * 0) + 1),lenP12)) ; :: thesis:
then A122: 1 <= n by FINSEQ_3:25;
A123: n <= len (P1 .cut (((2 * 0) + 1),lenP12)) by A121, FINSEQ_3:25;
then n < len (P1 .cut (((2 * 0) + 1),lenP12)) by XXREAL_0:1;
then A124: n + 1 <= len (P1 .cut (((2 * 0) + 1),lenP12)) by NAT_1:13;
1 <= n + 1 by A121, NAT_1:13;
then n + 1 in dom (P1 .cut (((2 * 0) + 1),lenP12)) by A124, FINSEQ_3:25;
then A125: (P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1) = P1 . (n + 1) by A119, GLIB_001:46;
len (P1 .cut (((2 * 0) + 1),lenP12)) = lenP12 by A119, GLIB_001:45;
then n <= len P1 by A119, A123, XXREAL_0:2;
then A126: n in dom P1 by A122, FINSEQ_3:25;
(P1 .cut (((2 * 0) + 1),lenP12)) . n = P1 . n by A119, A121, GLIB_001:46;
hence (P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1)) by A100, A125, A126; :: thesis:

end;

A127: lenP12 + (1 + 1) = len P1 by A116;
lenP12 + 1 = lenP11 by A116;
then A128: P1 .cut (lenP12,(len P1)) = G .walkOf (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),v) by A102, A115, A118, A119, A127, GLIB_001:40;
A129: P1 .cut (((2 * 0) + 1),lenP12) is_augmenting_wrt EL by A97, Th2;
A130: 1 <= lenP12 by ABIAN:12;
then A131: (P1 .cut (((2 * 0) + 1),lenP12)) .append (P1 .cut (lenP12,(len P1))) = P1 .cut (((2 * 0) + 1),(len P1)) by A119, GLIB_001:38
.= P1 by GLIB_001:39 ;
A132: lenP21 < (len P2) - 0 by XREAL_1:15;
3 - 2 <= lenP21 by A111, XREAL_1:15;
then A133: lenP21 in dom P2 by A132, FINSEQ_3:25;
lenP21 + 1 = len P2 ;
then A134: P2 . lenP21 = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A101, A104, A133, A108;
then consider lenP22 being odd Element of NAT such that
A135: lenP22 = lenP21 - 1 and
lenP21 - 1 in dom P2 and
lenP21 + 1 in dom P2 and
A136: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins P2 . lenP22,v,G by A104, A133, GLIB_001:9;
A137: lenP22 + (1 + 1) = len P2 by A135;
set P2A = P2 .cut (((2 * 0) + 1),lenP22);
A138: lenP22 < len P2 by A132, A135, XREAL_1:15;

A139: now :: thesis:

let n be even Nat; :: thesis:
assume A140: n in dom (P2 .cut (((2 * 0) + 1),lenP22)) ; :: thesis:
then A141: 1 <= n by FINSEQ_3:25;
A142: n <= len (P2 .cut (((2 * 0) + 1),lenP22)) by A140, FINSEQ_3:25;
then n < len (P2 .cut (((2 * 0) + 1),lenP22)) by XXREAL_0:1;
then A143: n + 1 <= len (P2 .cut (((2 * 0) + 1),lenP22)) by NAT_1:13;
1 <= n + 1 by A140, NAT_1:13;
then n + 1 in dom (P2 .cut (((2 * 0) + 1),lenP22)) by A143, FINSEQ_3:25;
then A144: (P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1) = P2 . (n + 1) by A138, GLIB_001:46;
len (P2 .cut (((2 * 0) + 1),lenP22)) = lenP22 by A138, GLIB_001:45;
then n <= len P2 by A138, A142, XXREAL_0:2;
then A145: n in dom P2 by A141, FINSEQ_3:25;
(P2 .cut (((2 * 0) + 1),lenP22)) . n = P2 . n by A138, A140, GLIB_001:46;
hence (P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1)) by A101, A144, A145; :: thesis:

end;

A146: 1 <= lenP22 by ABIAN:12;
then A147: (P2 .cut (((2 * 0) + 1),lenP22)) .append (P2 .cut (lenP22,(len P2))) = P2 .cut (((2 * 0) + 1),(len P2)) by A138, GLIB_001:38
.= P2 by GLIB_001:39 ;
A148: P2 . lenP22 = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A107, A136;
then A149: P2 .cut (((2 * 0) + 1),lenP22) is_Walk_from source,(the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A103, A146, A138, GLIB_001:37;
lenP22 + 1 = lenP21 by A135;
then A150: P2 .cut (lenP22,(len P2)) = G .walkOf (((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),v) by A104, A134, A148, A138, A137, GLIB_001:40;
A151: P2 .cut (((2 * 0) + 1),lenP22) is_augmenting_wrt EL by A99, Th2;
P1 .cut (((2 * 0) + 1),lenP12) is_Walk_from source,(the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A105, A118, A130, A119, GLIB_001:37;
hence P1 = P2 by A87, A92, A149, A129, A151, A120, A139, A128, A150, A131, A147; :: thesis:

end;

hence P1 = P2 ; :: thesis:

end;

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

end;

suppose A152: ( 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:

now :: thesis:

let v be set ; :: thesis:
let P1, P2 be vertex-distinct Path of G; :: thesis:
assume that
A158: v in dom ((AP:CompSeq (EL,source)) . (n + 1)) and
A159: P1 is_Walk_from source,v and
A160: P1 is_augmenting_wrt EL and
A161: P2 is_Walk_from source,v and
A162: P2 is_augmenting_wrt EL and
A163: for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) and
A164: for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ; :: thesis:
A165: P1 . (len P1) = v by A159, GLIB_001:17;
A166: P2 . 1 = source by A161, GLIB_001:17;
A167: P2 . (len P2) = v by A161, GLIB_001:17;
A168: P1 . 1 = source by A159, GLIB_001:17;

now :: thesis:

per cases by A157, A158, XBOOLE_0:def 3;

suppose v in dom ((AP:CompSeq (EL,source)) . n) ; :: thesis:

hence P1 = P2 by A87, A159, A160, A161, A162, A163, A164; :: thesis:

end;

suppose A169: v in {((the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n))} ; :: thesis:

then A170: v = (the_Target_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by TARSKI:def 1;
then ((AP:CompSeq (EL,source)) . (n + 1)) . v = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A156, Lm3;
then A171: (AP:FindAugPath (EL,source)) . v = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A158, Th7;
A172: v <> source by A155, A154, A169, TARSKI:def 1;
then P1 . 1 <> P1 .last() by A168, A165, GLIB_001:def 7;
then P1 .first() <> P1 .last() by GLIB_001:def 6;
then P1 is trivial by GLIB_001:127;
then A173: 3 <= len P1 by GLIB_001:125;
P2 . 1 <> P2 .last() by A166, A167, A172, GLIB_001:def 7;
then P2 .first() <> P2 .last() by GLIB_001:def 6;
then P2 is trivial by GLIB_001:127;
then A174: 3 <= len P2 by GLIB_001:125;
then A175: 3 - 2 < (len P2) - 0 by XREAL_1:15;
3 - 2 < (len P1) - 0 by A173, XREAL_1:15;
then reconsider lenP11 = (len P1) - 1, lenP21 = (len P2) - 1 as even Element of NAT by A175, INT_1:5;
A176: lenP11 < (len P1) - 0 by XREAL_1:15;
3 - 2 <= lenP11 by A173, XREAL_1:15;
then A177: lenP11 in dom P1 by A176, FINSEQ_3:25;
lenP11 + 1 = len P1 ;
then A178: P1 . lenP11 = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A163, A165, A177, A171;
then consider lenP12 being odd Element of NAT such that
A179: lenP12 = lenP11 - 1 and
lenP11 - 1 in dom P1 and
lenP11 + 1 in dom P1 and
A180: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins P1 . lenP12,v,G by A165, A177, GLIB_001:9;
A181: P1 . lenP12 = (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A170, A180;
set P1A = P1 .cut (((2 * 0) + 1),lenP12);
A182: lenP12 < len P1 by A176, A179, XREAL_1:15;

A183: now :: thesis:

let n be even Nat; :: thesis:
assume A184: n in dom (P1 .cut (((2 * 0) + 1),lenP12)) ; :: thesis:
then A185: 1 <= n by FINSEQ_3:25;
A186: n <= len (P1 .cut (((2 * 0) + 1),lenP12)) by A184, FINSEQ_3:25;
then n < len (P1 .cut (((2 * 0) + 1),lenP12)) by XXREAL_0:1;
then A187: n + 1 <= len (P1 .cut (((2 * 0) + 1),lenP12)) by NAT_1:13;
1 <= n + 1 by A184, NAT_1:13;
then n + 1 in dom (P1 .cut (((2 * 0) + 1),lenP12)) by A187, FINSEQ_3:25;
then A188: (P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1) = P1 . (n + 1) by A182, GLIB_001:46;
len (P1 .cut (((2 * 0) + 1),lenP12)) = lenP12 by A182, GLIB_001:45;
then n <= len P1 by A182, A186, XXREAL_0:2;
then A189: n in dom P1 by A185, FINSEQ_3:25;
(P1 .cut (((2 * 0) + 1),lenP12)) . n = P1 . n by A182, A184, GLIB_001:46;
hence (P1 .cut (((2 * 0) + 1),lenP12)) . n = (AP:FindAugPath (EL,source)) . ((P1 .cut (((2 * 0) + 1),lenP12)) . (n + 1)) by A163, A188, A189; :: thesis:

end;

A190: lenP12 + (1 + 1) = len P1 by A179;
lenP12 + 1 = lenP11 by A179;
then A191: P1 .cut (lenP12,(len P1)) = G .walkOf (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),v) by A165, A178, A181, A182, A190, GLIB_001:40;
A192: P1 .cut (((2 * 0) + 1),lenP12) is_augmenting_wrt EL by A160, Th2;
A193: 1 <= lenP12 by ABIAN:12;
then A194: (P1 .cut (((2 * 0) + 1),lenP12)) .append (P1 .cut (lenP12,(len P1))) = P1 .cut (((2 * 0) + 1),(len P1)) by A182, GLIB_001:38
.= P1 by GLIB_001:39 ;
A195: lenP21 < (len P2) - 0 by XREAL_1:15;
3 - 2 <= lenP21 by A174, XREAL_1:15;
then A196: lenP21 in dom P2 by A195, FINSEQ_3:25;
lenP21 + 1 = len P2 ;
then A197: P2 . lenP21 = the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A164, A167, A196, A171;
then consider lenP22 being odd Element of NAT such that
A198: lenP22 = lenP21 - 1 and
lenP21 - 1 in dom P2 and
lenP21 + 1 in dom P2 and
A199: the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) Joins P2 . lenP22,v,G by A167, A196, GLIB_001:9;
A200: lenP22 + (1 + 1) = len P2 by A198;
set P2A = P2 .cut (((2 * 0) + 1),lenP22);
A201: lenP22 < len P2 by A195, A198, XREAL_1:15;

A202: now :: thesis:

let n be even Nat; :: thesis:
assume A203: n in dom (P2 .cut (((2 * 0) + 1),lenP22)) ; :: thesis:
then A204: 1 <= n by FINSEQ_3:25;
A205: n <= len (P2 .cut (((2 * 0) + 1),lenP22)) by A203, FINSEQ_3:25;
then n < len (P2 .cut (((2 * 0) + 1),lenP22)) by XXREAL_0:1;
then A206: n + 1 <= len (P2 .cut (((2 * 0) + 1),lenP22)) by NAT_1:13;
1 <= n + 1 by A203, NAT_1:13;
then n + 1 in dom (P2 .cut (((2 * 0) + 1),lenP22)) by A206, FINSEQ_3:25;
then A207: (P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1) = P2 . (n + 1) by A201, GLIB_001:46;
len (P2 .cut (((2 * 0) + 1),lenP22)) = lenP22 by A201, GLIB_001:45;
then n <= len P2 by A201, A205, XXREAL_0:2;
then A208: n in dom P2 by A204, FINSEQ_3:25;
(P2 .cut (((2 * 0) + 1),lenP22)) . n = P2 . n by A201, A203, GLIB_001:46;
hence (P2 .cut (((2 * 0) + 1),lenP22)) . n = (AP:FindAugPath (EL,source)) . ((P2 .cut (((2 * 0) + 1),lenP22)) . (n + 1)) by A164, A207, A208; :: thesis:

end;

A209: 1 <= lenP22 by ABIAN:12;
then A210: (P2 .cut (((2 * 0) + 1),lenP22)) .append (P2 .cut (lenP22,(len P2))) = P2 .cut (((2 * 0) + 1),(len P2)) by A201, GLIB_001:38
.= P2 by GLIB_001:39 ;
A211: P2 . lenP22 = (the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A170, A199;
then A212: P2 .cut (((2 * 0) + 1),lenP22) is_Walk_from source,(the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A166, A209, A201, GLIB_001:37;
lenP22 + 1 = lenP21 by A198;
then A213: P2 .cut (lenP22,(len P2)) = G .walkOf (((the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n)), the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n),v) by A167, A197, A211, A201, A200, GLIB_001:40;
A214: P2 .cut (((2 * 0) + 1),lenP22) is_augmenting_wrt EL by A162, Th2;
P1 .cut (((2 * 0) + 1),lenP12) is_Walk_from source,(the_Source_of G) . the Element of AP:NextBestEdges ((AP:CompSeq (EL,source)) . n) by A168, A181, A193, A182, GLIB_001:37;
hence P1 = P2 by A87, A152, A212, A192, A214, A183, A202, A191, A213, A194, A210; :: thesis:

end;

hence P1 = P2 ; :: thesis:

end;

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

end;

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

end;

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

now :: thesis:

let v be set ; :: thesis:
let P1, P2 be vertex-distinct Path of G; :: thesis:
assume that
A216: v in dom ((AP:CompSeq (EL,source)) . 0) and
A217: P1 is_Walk_from source,v and
P1 is_augmenting_wrt EL and
A218: P2 is_Walk_from source,v and
P2 is_augmenting_wrt EL and
for n being even Nat st n in dom P1 holds
P1 . n = (AP:FindAugPath (EL,source)) . (P1 . (n + 1)) and
for n being even Nat st n in dom P2 holds
P2 . n = (AP:FindAugPath (EL,source)) . (P2 . (n + 1)) ; :: thesis:
v in {source} by A216, Th4;
then A219: v = source by TARSKI:def 1;
then A220: P1 . ((2 * 0) + 1) = v by A217, GLIB_001:17;
A221: P2 . ((2 * 0) + 1) = v by A218, A219, GLIB_001:17;
A222: 1 <= len P1 by ABIAN:12;
P1 . (len P1) = v by A217, GLIB_001:17;
then len P1 = 1 by A220, A222, GLIB_001:def 29;
then A223: P1 = <*v*> by A220, FINSEQ_1:40;
A224: 1 <= len P2 by ABIAN:12;
P2 . (len P2) = v by A218, GLIB_001:17;
then len P2 = 1 by A221, A224, GLIB_001:def 29;
hence P1 = P2 by A221, A223, FINSEQ_1:40; :: thesis:

end;

then A225: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A225, A215);
hence ( sink in dom (AP:FindAugPath (EL,source)) & IT1 is_Walk_from source,sink & IT1 is_augmenting_wrt EL & ( for n being even Nat st n in dom IT1 holds
IT1 . n = (AP:FindAugPath (EL,source)) . (IT1 . (n + 1)) ) & IT2 is_Walk_from source,sink & IT2 is_augmenting_wrt EL & ( for n being even Nat st n in dom IT2 holds
IT2 . n = (AP:FindAugPath (EL,source)) . (IT2 . (n + 1)) ) implies IT1 = IT2 ) ; :: thesis:
thus ( not sink in dom (AP:FindAugPath (EL,source)) & IT1 = G .walkOf source & IT2 = G .walkOf source implies IT1 = IT2 ) ; :: thesis: