( dom {} c= the_Vertices_of G & rng {} c= NAT ) by XBOOLE_1:2;
then A: {} in PFuncs (the_Vertices_of G),NAT by PARTFUN1:def 5;
set f = (the_Vertices_of G) --> 0 ;
B: dom ((the_Vertices_of G) --> 0 ) = the_Vertices_of G by FUNCOP_1:19;
rng ((the_Vertices_of G) --> 0 ) c= NAT ;
then (the_Vertices_of G) --> 0 in Funcs (the_Vertices_of G),NAT by B, FUNCT_2:def 2;
hence [{} ,((the_Vertices_of G) --> 0 )] is MCS:Labeling of G by A, ZFMISC_1:def 2; :: thesis: verum