let G be finite _Graph; :: thesis: ((MCS:CSeq G) ``1 ) .Lifespan() = (MCS:CSeq G) .Lifespan()
set S = MCS:CSeq G;
set VN = (MCS:CSeq G) ``1 ;
set ls = G .order() ;
AA: (MCS:CSeq G) .Lifespan() = G .order() by Th87;
AHa: (MCS:CSeq G) ``1 is eventually-constant by mVNS0a;
Aa: ( ((MCS:CSeq G) . (G .order() )) `1 = ((MCS:CSeq G) ``1 ) . (G .order() ) & ((MCS:CSeq G) . ((G .order() ) + 1)) `1 = ((MCS:CSeq G) ``1 ) . ((G .order() ) + 1) ) by d1stMCSLS;
A: ((MCS:CSeq G) ``1 ) . (G .order() ) = ((MCS:CSeq G) ``1 ) . ((G .order() ) + 1) by Th83, Aa, NAT_1:11;

B: now

let n be Nat; :: thesis: ( ((MCS:CSeq G) ``1 ) . n = ((MCS:CSeq G) ``1 ) . (n + 1) implies not G .order() > n )
assume that
A1: ((MCS:CSeq G) ``1 ) . n = ((MCS:CSeq G) ``1 ) . (n + 1) and
B1: G .order() > n ; :: thesis: contradiction
n + 1 <= G .order() by B1, NAT_1:13;
then C1: ( card (dom (((MCS:CSeq G) . n) `1 )) = n & card (dom (((MCS:CSeq G) . (n + 1)) `1 )) = n + 1 ) by B1, Th82;
( ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1 ) . n & ((MCS:CSeq G) . (n + 1)) `1 = ((MCS:CSeq G) ``1 ) . (n + 1) ) by d1stMCSLS;
hence contradiction by C1, A1; :: thesis: verum

end;

thus ((MCS:CSeq G) ``1 ) .Lifespan() = (MCS:CSeq G) .Lifespan() by AA, AHa, A, B, GLIB_000:def 57; :: thesis: verum