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

now :: thesis: for n, x being set ex y being set st S₁[n,x,y]

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

now :: thesis: ex y being set st S₁[n,x,y]

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

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

then consider e being FF:ELabeling of G 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 G 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 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 Nat holds S₁[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A2);
reconsider IT = IT as ManySortedSet of NAT by A3, PARTFUN1:def 2, RELAT_1:def 18;
defpred S₂[ Nat] means ex Gn being FF:ELabeling of G st IT . $1 = Gn;

A4: 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 S₂[n] ; :: thesis: S₂[n + 1]
then consider Gn being FF:ELabeling of G such that
A5: IT . n = Gn ;
S₁[n,Gn,IT . (n + 1)] by A3, A5;
hence S₂[n + 1] ; :: thesis: verum

end;

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

now :: thesis: for n being Nat holds IT . n is FF:ELabeling of G

let n be Nat; :: thesis: IT . n is FF:ELabeling of G
ex Gn being FF:ELabeling of G st IT . n = Gn by A7;
hence IT . n is FF:ELabeling of G ; :: 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 n9 = n as Element of NAT by ORDINAL1:def 12;
ex X being FF:ELabeling of G st
( X = IT . n & IT . (n9 + 1) = FF:Step (X,source,sink) ) by A3;
hence IT . (n + 1) = FF:Step ((IT . n),source,sink) ; :: thesis: verum