let G be finite _Graph; :: thesis: dom (((LexBFS:CSeq G) .Result() ) `1 ) = the_Vertices_of G
set CS = LexBFS:CSeq G;
set CSO = (LexBFS:CSeq G) . (G .order() );
(LexBFS:CSeq G) .Result() = (LexBFS:CSeq G) . (G .order() ) by Th37;
hence dom (((LexBFS:CSeq G) .Result() ) `1 ) = the_Vertices_of G by Th36; :: thesis: verum