now :: thesis: for x being object st x in dom (G .inDegreeMap()) holds
(G .inDegreeMap()) . x is natural

let x be object ; :: thesis: ( x in dom (G .inDegreeMap()) implies (G .inDegreeMap()) . x is natural )
assume x in dom (G .inDegreeMap()) ; :: thesis: (G .inDegreeMap()) . x is natural
then reconsider v = x as Vertex of G ;
(G .inDegreeMap()) . x = v .inDegree() by Def12;
hence (G .inDegreeMap()) . x is natural ; :: thesis: verum

end;

hence G .inDegreeMap() is natural-valued by VALUED_0:def 12; :: thesis: verum