let G be finite _Graph; :: thesis: ((LexBFS:CSeq G) ``1 ) .Lifespan() = (LexBFS:CSeq G) .Lifespan()
set S = LexBFS:CSeq G;
set VN = (LexBFS:CSeq G) ``1 ;
set ls = G .order() ;
A1: (LexBFS:CSeq G) ``1 is eventually-constant by Th38;
A2: ((LexBFS:CSeq G) . ((G .order() ) + 1)) `1 = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) + 1) by Def16;

A3: now

let n be Nat; :: thesis: ( ((LexBFS:CSeq G) ``1 ) . n = ((LexBFS:CSeq G) ``1 ) . (n + 1) implies not G .order() > n )
assume that
A4: ((LexBFS:CSeq G) ``1 ) . n = ((LexBFS:CSeq G) ``1 ) . (n + 1) and
A5: G .order() > n ; :: thesis: contradiction
n + 1 <= G .order() by A5, NAT_1:13;
then A6: card (dom (((LexBFS:CSeq G) . (n + 1)) `1 )) = n + 1 by Th32;
A7: ((LexBFS:CSeq G) . (n + 1)) `1 = ((LexBFS:CSeq G) ``1 ) . (n + 1) by Def16;
A8: ((LexBFS:CSeq G) . n) `1 = ((LexBFS:CSeq G) ``1 ) . n by Def16;
card (dom (((LexBFS:CSeq G) . n) `1 )) = n by A5, Th32;
hence contradiction by A4, A6, A8, A7; :: thesis: verum

end;

((LexBFS:CSeq G) . (G .order() )) `1 = ((LexBFS:CSeq G) ``1 ) . (G .order() ) by Def16;
then A9: ((LexBFS:CSeq G) ``1 ) . (G .order() ) = ((LexBFS:CSeq G) ``1 ) . ((G .order() ) + 1) by A2, Th33, NAT_1:11;
(LexBFS:CSeq G) .Lifespan() = G .order() by Th37;
hence ((LexBFS:CSeq G) ``1 ) .Lifespan() = (LexBFS:CSeq G) .Lifespan() by A1, A9, A3, GLIB_000:def 57; :: thesis: verum