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 Def15;

A3: now :: thesis: for n being Nat st ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . (n + 1) holds
not G .order() > n

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 Def15;
A8: ((LexBFS:CSeq G) . n) `1 = ((LexBFS:CSeq G) ``1) . n by Def15;
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 Def15;
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 56; :: thesis: verum