set f = (the_Vertices_of G) --> {} ;
A1: rng {} c= NAT ;
{} c= NAT ;
then {} in Fin NAT by FINSUB_1:def 5;
then {{} } c= Fin NAT by ZFMISC_1:37;
then A2: rng ((the_Vertices_of G) --> {} ) c= Fin NAT by XBOOLE_1:1;
dom ((the_Vertices_of G) --> {} ) = the_Vertices_of G by FUNCOP_1:19;
then A3: (the_Vertices_of G) --> {} in Funcs (the_Vertices_of G),(Fin NAT ) by A2, FUNCT_2:def 2;
dom {} c= the_Vertices_of G by XBOOLE_1:2;
then {} in PFuncs (the_Vertices_of G),NAT by A1, PARTFUN1:def 5;
hence [{} ,((the_Vertices_of G) --> {} )] is LexBFS:Labeling of G by A3, ZFMISC_1:def 2; :: thesis: verum