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

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

end;

hence G .degreeMap() is Cardinal-yielding by CARD_3:def 1; :: thesis: verum