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