dom (G .inDegreeMap()) = the_Vertices_of G by PARTFUN1:def 2
.= rng v by FUNCT_2:def 3 ;
then A2: dom ((G .inDegreeMap()) * v) = dom v by RELAT_1:27
.= G .order() by FUNCT_2:def 1 ;
then card (dom ((G .inDegreeMap()) * v)) = G .order() ;
then card ((G .inDegreeMap()) * v) = G .order() by CARD_1:62;
hence ( (G .inDegreeMap()) * v is Sequence-like & (G .inDegreeMap()) * v is G .order() -element ) by A2, ORDINAL1:def 7, CARD_1:def 7; :: thesis: verum