A1: dom (G .degreeMap()) = the_Vertices_of G by PARTFUN1:def 2;
rng (G .degreeMap()) c= NAT by VALUED_0:def 6;
hence G .degreeMap() is Function of (the_Vertices_of G),NAT by A1, FUNCT_2:2; :: thesis: verum