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

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

end;

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