set f = (the_Vertices_of G) --> 0;
A1: rng {} c= NAT ;
A2: rng ((the_Vertices_of G) --> 0) c= NAT ;
dom ((the_Vertices_of G) --> 0) = the_Vertices_of G ;
then A3: (the_Vertices_of G) --> 0 in Funcs ((the_Vertices_of G),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) --> 0)] is MCS:Labeling of G by A3, ZFMISC_1:def 2; :: thesis: verum