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