let G be _finite _Graph; :: thesis: (LexBFS:CSeq G) ``1 is eventually-constant

set CS = LexBFS:CSeq G;

set S = (LexBFS:CSeq G) ``1 ;

set CS = LexBFS:CSeq G;

set S = (LexBFS:CSeq G) ``1 ;

now :: thesis: ex n being Nat st

for m being Nat st n <= m holds

((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

hence
(LexBFS:CSeq G) ``1 is eventually-constant
; :: thesis: verumfor m being Nat st n <= m holds

((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

consider n being Nat such that

A1: for m being Nat st n <= m holds

(LexBFS:CSeq G) . n = (LexBFS:CSeq G) . m by Def6;

take n = n; :: thesis: for m being Nat st n <= m holds

((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

let m be Nat; :: thesis: ( n <= m implies ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m )

assume A2: n <= m ; :: thesis: ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

thus ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) . n) `1 by Def15

.= ((LexBFS:CSeq G) . m) `1 by A1, A2

.= ((LexBFS:CSeq G) ``1) . m by Def15 ; :: thesis: verum

end;A1: for m being Nat st n <= m holds

(LexBFS:CSeq G) . n = (LexBFS:CSeq G) . m by Def6;

take n = n; :: thesis: for m being Nat st n <= m holds

((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

let m be Nat; :: thesis: ( n <= m implies ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m )

assume A2: n <= m ; :: thesis: ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) ``1) . m

thus ((LexBFS:CSeq G) ``1) . n = ((LexBFS:CSeq G) . n) `1 by Def15

.= ((LexBFS:CSeq G) . m) `1 by A1, A2

.= ((LexBFS:CSeq G) ``1) . m by Def15 ; :: thesis: verum