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:31;

then A2: rng ((the_Vertices_of G) --> {}) c= Fin NAT ;

dom ((the_Vertices_of G) --> {}) = the_Vertices_of G ;

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 ;

then {} in PFuncs ((the_Vertices_of G),NAT) by A1, PARTFUN1:def 3;

hence [{},((the_Vertices_of G) --> {})] is LexBFS:Labeling of G by A3, ZFMISC_1:def 2; :: thesis: verum

A1: rng {} c= NAT ;

{} c= NAT ;

then {} in Fin NAT by FINSUB_1:def 5;

then {{}} c= Fin NAT by ZFMISC_1:31;

then A2: rng ((the_Vertices_of G) --> {}) c= Fin NAT ;

dom ((the_Vertices_of G) --> {}) = the_Vertices_of G ;

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 ;

then {} in PFuncs ((the_Vertices_of G),NAT) by A1, PARTFUN1:def 3;

hence [{},((the_Vertices_of G) --> {})] is LexBFS:Labeling of G by A3, ZFMISC_1:def 2; :: thesis: verum