let G be _finite _Graph; :: thesis: (MCS:CSeq G) ``1 is eventually-constant
set CS = MCS:CSeq G;
set S = (MCS:CSeq G) ``1 ;

now :: thesis: ex n being Nat st
for m being Nat st n <= m holds
((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) ``1) . m

consider n being Nat such that
A1: for m being Nat st n <= m holds
(MCS:CSeq G) . n = (MCS:CSeq G) . m by Def6;
take n = n; :: thesis: for m being Nat st n <= m holds
((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) ``1) . m
let m be Nat; :: thesis: ( n <= m implies ((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) ``1) . m )
assume A2: n <= m ; :: thesis: ((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) ``1) . m
thus ((MCS:CSeq G) ``1) . n = ((MCS:CSeq G) . n) `1 by Def24
.= ((MCS:CSeq G) . m) `1 by A1, A2
.= ((MCS:CSeq G) ``1) . m by Def24 ; :: thesis: verum

end;

hence (MCS:CSeq G) ``1 is eventually-constant ; :: thesis: verum