defpred S1[ set , set , set ] means ( ( $2 is DIJK:Labeling of G & ex Gn, Gn1 being DIJK:Labeling of G st
( $2 = Gn & $3 = Gn1 & Gn1 = DIJK:Step Gn ) ) or ( $2 is not DIJK:Labeling of G & $2 = $3 ) );
now :: thesis: for n being Nat
for x being set ex y being set st S1[n,x,y]
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
now :: thesis: ex y being set st S1[n,x,y]
per cases ( x is DIJK:Labeling of G or not x is DIJK:Labeling of G ) ;
suppose x is DIJK:Labeling of G ; :: thesis: ex y being set st S1[n,x,y]
then reconsider Gn = x as DIJK:Labeling of G ;
S1[n,x, DIJK:Step Gn] ;
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
suppose x is not DIJK:Labeling of G ; :: thesis: ex y being set st S1[n,x,y]
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
end;
end;
hence ex y being set st S1[n,x,y] ; :: thesis: verum
end;
then A1: for n being Nat
for x being set ex y being set st S1[n,x,y] ;
consider IT being Function such that
A2: ( dom IT = NAT & IT . 0 = DIJK:Init src & ( for n being Nat holds S1[n,IT . n,IT . (n + 1)] ) ) from RECDEF_1:sch 1(A1);
 reconsider IT = IT as ManySortedSet of NAT by A2, PARTFUN1:def 2, RELAT_1:def 18;
defpred S2[ Nat] means IT . $1 is DIJK:Labeling of G;
A3: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A4: S2[n] ; :: thesis: S2[n + 1]
ex Gn, Gn1 being DIJK:Labeling of G st
( IT . n = Gn & IT . (n + 1) = Gn1 & Gn1 = DIJK:Step Gn ) by A2, A4;
hence S2[n + 1] ; :: thesis: verum
end;
A5: S2[ 0 ] by A2;
for n being Nat holds S2[n] from NAT_1:sch 2(A5, A3);
 then reconsider IT = IT as DIJK:LabelingSeq of G by Def10;
reconsider IT = IT as DIJK:LabelingSeq of G ;
take IT ; :: thesis: ( IT . 0 = DIJK:Init src & ( for n being Nat holds IT . (n + 1) = DIJK:Step (IT . n) ) )
thus IT . 0 = DIJK:Init src by A2; :: thesis: for n being Nat holds IT . (n + 1) = DIJK:Step (IT . n)
let n be Nat; :: thesis: IT . (n + 1) = DIJK:Step (IT . n)
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
ex Gn, Gn1 being DIJK:Labeling of G st
( IT . n9 = Gn & IT . (n + 1) = Gn1 & Gn1 = DIJK:Step Gn ) by A2;
hence IT . (n + 1) = DIJK:Step (IT . n) ; :: thesis: verum