let G be finite _Graph; :: thesis: for n being Nat st G .order() <= n holds
(LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) . n
let n be Nat; :: thesis: ( G .order() <= n implies (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) . n )
assume A1: G .order() <= n ; :: thesis: (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) . n
set CS = LexBFS:CSeq G;
defpred S₁[ Nat] means G .order() = card (dom (((LexBFS:CSeq G) . ((G .order() ) + $1)) `1 ));
A2: S₁[ 0 ] by Th46;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
set CSK = (LexBFS:CSeq G) . ((G .order() ) + k);
set VLK = ((LexBFS:CSeq G) . ((G .order() ) + k)) `1 ;
set CK1 = (LexBFS:CSeq G) . (((G .order() ) + k) + 1);
(LexBFS:CSeq G) . (((G .order() ) + k) + 1) = LexBFS:Step ((LexBFS:CSeq G) . ((G .order() ) + k)) by Def33;
hence S₁[k + 1] by A4, Def32; :: thesis: verum

end;

A6: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
defpred S₂[ Nat] means (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) . ((G .order() ) + $1);
A7: S₂[ 0 ] ;
A8: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A9: S₂[k] ; :: thesis: S₂[k + 1]
set CSK = (LexBFS:CSeq G) . ((G .order() ) + k);
set VLK = ((LexBFS:CSeq G) . ((G .order() ) + k)) `1 ;
set CK1 = (LexBFS:CSeq G) . (((G .order() ) + k) + 1);
A10: card (dom (((LexBFS:CSeq G) . ((G .order() ) + k)) `1 )) = G .order() by A6;
(LexBFS:CSeq G) . (((G .order() ) + k) + 1) = LexBFS:Step ((LexBFS:CSeq G) . ((G .order() ) + k)) by Def33;
hence S₂[k + 1] by A9, A10, Def32; :: thesis: verum

end;

A11: for k being Nat holds S₂[k] from NAT_1:sch 2(A7, A8);
ex i being Nat st (G .order() ) + i = n by A1, NAT_1:10;
hence (LexBFS:CSeq G) . (G .order() ) = (LexBFS:CSeq G) . n by A11; :: thesis: verum