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

A1: now :: thesis: for i being object st i in NAT holds
ex r being object st S₁[i,r]

let i be object ; :: thesis: ( i in NAT implies ex r being object st S₁[i,r] )
assume i in NAT ; :: thesis: ex r being object st S₁[i,r]
reconsider r = [{},{}] as object ;
take r = 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 ;
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 object 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