defpred S₁[ set , set ] means $2 is DIJK:Labeling of G;

A: now

let i be set ; :: thesis: ( i in NAT implies ex r being set st S₁[i,r] )
assume i in NAT ; :: thesis: ex r being set st S₁[i,r]
take r = [{} ,{} ]; :: thesis: S₁[i,r]
{} is PartFunc of (the_Vertices_of G),REAL by RELSET_1:25;
then B1: {} in PFuncs (the_Vertices_of G),REAL by PARTFUN1:119;
{} c= the_Edges_of G by XBOOLE_1:2;
hence S₁[i,r] by B1, ZFMISC_1:def 2; :: thesis: verum

end;

consider s being ManySortedSet of such that
Z: for i being set st i in NAT holds
S₁[i,s . i] from PBOOLE:sch 3(A);
take s ; :: thesis: for n being Nat holds s . n is DIJK:Labeling of G
let i be Nat; :: thesis: s . i is DIJK:Labeling of G
i in NAT by ORDINAL1:def 13;
hence s . i is DIJK:Labeling of G by Z; :: thesis: verum