defpred S1[ 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 for n, x being set ex y being set st S1[n,x,y]let n,
x be
set ;
ex y being set st S1[n,x,y]now ex y being set st S1[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
;
ex y being set st S1[n,x,y]then consider e being
FF:ELabeling of
G such that A1:
e = x
;
set y =
FF:Step (
e,
source,
sink);
S1[
n,
x,
FF:Step (
e,
source,
sink)]
by A1;
hence
ex
y being
set st
S1[
n,
x,
y]
;
verum end; end; end; hence
ex
y being
set st
S1[
n,
x,
y]
;
verum end;
then A2:
for n being Nat
for x being set ex y being set st S1[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 S1[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 S2[ Nat] means ex Gn being FF:ELabeling of G st IT . $1 = Gn;
A4:
now for n being Nat st S2[n] holds
S2[n + 1]let n be
Nat;
( S2[n] implies S2[n + 1] )assume
S2[
n]
;
S2[n + 1]then consider Gn being
FF:ELabeling of
G such that A5:
IT . n = Gn
;
S1[
n,
Gn,
IT . (n + 1)]
by A3, A5;
hence
S2[
n + 1]
;
verum end;
A6:
S2[ 0 ]
by A3;
A7:
for n being Nat holds S2[n]
from NAT_1:sch 2(A6, A4);
then reconsider IT = IT as FF:ELabelingSeq of G by Def19;
take
IT
; ( 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; for n being Nat holds IT . (n + 1) = FF:Step ((IT . n),source,sink)
let n be Nat; 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)
; verum