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

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

end;

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