defpred S₁[ set , set , set ] means ( ex e being FF:ELabeling of st
( e = $2 & $3 = FF:Step e,source,sink ) or ( ( for e being FF:ELabeling of holds not e = $2 ) & $3 = $2 ) );

now

let n, x be set ; :: thesis: ex y being set st S₁[n,x,y]

now

per cases ( ex e being FF:ELabeling of st e = x or for e being FF:ELabeling of holds not e = x ) ;

suppose ex e being FF:ELabeling of st e = x ; :: thesis: ex y being set st S₁[n,x,y]

then consider e being FF:ELabeling of such that
A1: e = x ;
set y = FF:Step e,source,sink;
S₁[n,x, FF:Step e,source,sink] by A1;
hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

suppose for e being FF:ELabeling of holds not e = x ; :: thesis: ex y being set st S₁[n,x,y]

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

end;

end;

hence ex y being set st S₁[n,x,y] ; :: thesis: verum

end;

then A2: for n being Element of NAT
for x being set ex y being set st S₁[n,x,y] ;
consider IT being Function such that
A3: ( dom IT = NAT & IT . 0 = (the_Edges_of G) --> 0 & ( for n being Element of NAT holds S₁[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A2);
reconsider IT = IT as ManySortedSet of by A3, PARTFUN1:def 4, RELAT_1:def 18;
defpred S₂[ Nat] means ex Gn being FF:ELabeling of st IT . $1 = Gn;

A4: now

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume S₂[n] ; :: thesis: S₂[n + 1]
then consider Gn being FF:ELabeling of such that
A5: IT . n = Gn ;
n in NAT by ORDINAL1:def 13;
then S₁[n,Gn,IT . (n + 1)] by A3, A5;
hence S₂[n + 1] ; :: thesis: verum
set P = AP:GetAugPath Gn,source,sink;

end;

A6: S₂[ 0 ] by A3;
A7: for n being Nat holds S₂[n] from NAT_1:sch 2(A6, A4);

now

let n be Nat; :: thesis: IT . n is FF:ELabeling of
ex Gn being FF:ELabeling of st IT . n = Gn by A7;
hence IT . n is FF:ELabeling of ; :: thesis: verum

end;

then reconsider IT = IT as FF:ELabelingSeq of G by Def19;
take IT ; :: thesis: ( IT . 0 = (the_Edges_of G) --> 0 & ( for n being Nat holds IT . (n + 1) = FF:Step (IT . n),source,sink ) )
thus IT . 0 = (the_Edges_of G) --> 0 by A3; :: thesis: for n being Nat holds IT . (n + 1) = FF:Step (IT . n),source,sink
let n be Nat; :: thesis: IT . (n + 1) = FF:Step (IT . n),source,sink
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
ex X being FF:ELabeling of st
( X = IT . n & IT . (n' + 1) = FF:Step X,source,sink ) by A3;
hence IT . (n + 1) = FF:Step (IT . n),source,sink ; :: thesis: verum
reconsider E0 = (the_Edges_of G) --> 0 as Function of (the_Edges_of G),REAL by FUNCOP_1:58;