set f = src .--> 0;
( dom (src .--> 0) = {src} & rng (src .--> 0) = {0} ) by FUNCOP_1:8;
then A1: src .--> 0 in PFuncs ((the_Vertices_of G),REAL) by PARTFUN1:def 3;
{} c= the_Edges_of G ;
hence [(src .--> 0),{}] is DIJK:Labeling of G by A1, ZFMISC_1:def 2; :: thesis: verum