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

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

end;

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