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