set f = src .--> 0 ;
( dom (src .--> 0 ) = {src} & rng (src .--> 0 ) = {0 } ) by FUNCOP_1:14, FUNCOP_1:19;
then A1: src .--> 0 in PFuncs (the_Vertices_of G),REAL by PARTFUN1:def 5;
{} 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