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