let G be finite _Graph; :: thesis: (((LexBFS:CSeq G) .Result() ) `1 ) " is VertexScheme of G
set CS = LexBFS:CSeq G;
set CSO = (LexBFS:CSeq G) . (G .order() );
set VLO = ((LexBFS:CSeq G) . (G .order() )) `1 ;
set VL = (LexBFS:CSeq G) ``1 ;
A2: (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) .Result() by Th51;
AA: ((LexBFS:CSeq G) . (G .order() )) `1 = ((LexBFS:CSeq G) ``1 ) . (G .order() ) by d1stBFSLS;
A3: ((LexBFS:CSeq G) . (G .order() )) `1 is one-to-one by AA, Th25;
A4: dom (((LexBFS:CSeq G) . (G .order() )) `1 ) = the_Vertices_of G by Th50;
AB: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1 ) .Lifespan() by VNS0;
(LexBFS:CSeq G) .Lifespan() = G .order() by Th51;
then rng (((LexBFS:CSeq G) ``1 ) . (G .order() )) = (Seg (G .order() )) \ (Seg ((G .order() ) -' (G .order() ))) by AB, Th21
.= (Seg (G .order() )) \ (Seg 0 ) by XREAL_1:234
.= Seg (G .order() ) ;
then A5: ( rng ((((LexBFS:CSeq G) . (G .order() )) `1 ) " ) = the_Vertices_of G & dom ((((LexBFS:CSeq G) . (G .order() )) `1 ) " ) = Seg (G .order() ) ) by AA, A3, A4, FUNCT_1:55;
then (((LexBFS:CSeq G) . (G .order() )) `1 ) " is FinSequence by FINSEQ_1:def 2;
then A6: (((LexBFS:CSeq G) . (G .order() )) `1 ) " is FinSequence of the_Vertices_of G by A5, FINSEQ_1:def 4;
thus (((LexBFS:CSeq G) .Result() ) `1 ) " is VertexScheme of G by A2, A3, A5, A6, CHORD:def 12; :: thesis: verum