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

A1: 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:12;
then A2: {} in PFuncs ((the_Vertices_of G),REAL) by PARTFUN1:45;
{} c= the_Edges_of G by XBOOLE_1:2;
hence S₁[i,r] by A2, ZFMISC_1:def 2; :: thesis: verum

end;

consider s being ManySortedSet of NAT such that
A3: for i being set st i in NAT holds
S₁[i,s . i] from PBOOLE:sch 3(A1);
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 12;
hence s . i is DIJK:Labeling of G by A3; :: thesis: verum