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 G .order() <= n ; :: thesis: (LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . n
then A1: ex i being Nat st (G .order()) + i = n by NAT_1:10;
set CS = LexBFS:CSeq G;
defpred S₁[ Nat] means G .order() = card (dom (((LexBFS:CSeq G) . ((G .order()) + $1)) `1));
defpred S₂[ Nat] means (LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . ((G .order()) + $1);
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set CK1 = (LexBFS:CSeq G) . (((G .order()) + k) + 1);
set CSK = (LexBFS:CSeq G) . ((G .order()) + k);
(LexBFS:CSeq G) . (((G .order()) + k) + 1) = LexBFS:Step ((LexBFS:CSeq G) . ((G .order()) + k)) by Def16;
hence S₁[k + 1] by A3, Def13; :: thesis: verum

end;

A4: S₁[ 0 ] by Th32;
A5: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
A6: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A7: S₂[k] ; :: thesis: S₂[k + 1]
set CK1 = (LexBFS:CSeq G) . (((G .order()) + k) + 1);
set CSK = (LexBFS:CSeq G) . ((G .order()) + k);
set VLK = ((LexBFS:CSeq G) . ((G .order()) + k)) `1 ;
A8: (LexBFS:CSeq G) . (((G .order()) + k) + 1) = LexBFS:Step ((LexBFS:CSeq G) . ((G .order()) + k)) by Def16;
card (dom (((LexBFS:CSeq G) . ((G .order()) + k)) `1)) = G .order() by A5;
hence S₂[k + 1] by A7, A8, Def13; :: thesis: verum

end;

A9: S₂[ 0 ] ;
for k being Nat holds S₂[k] from NAT_1:sch 2(A9, A6);
hence (LexBFS:CSeq G) . (G .order()) = (LexBFS:CSeq G) . n by A1; :: thesis: verum