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